Theory Intro_Dest_Elim.IHOL_IDE

(* Copyright 2021 (C) Mihails Milehins *)

sectionIHOL_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