Theory Intro_Dest_Elim.IHOL_IDE

(* Copyright 2021 (C) Mihails Milehins *)

section‹‹IHOL_IDE››
theory IHOL_IDE
  imports Main
  keywords "mk_ide" :: thy_defn
    and "rf"
    and "|intro" "|dest" "|elim" 
begin



subsection‹Miscellaneous results›
           
lemma PQ_P_Q: "P ≡ Q ⟹ P ⟹ Q" by auto
    


subsection‹Import›

ML_file‹IDE.ML›

end