Theory IHOL_IDE

(* Copyright 2021 (C) Mihails Milehins *)

sectionIHOL_IDE›
theory IHOL_IDE
  imports "IDE_Tools/IDE_Tools"
  keywords "mk_ide" :: thy_defn
    and "rf"
    and "|intro" "|dest" "|elim" 
begin



subsectionMiscellaneous results
           
lemma PQ_P_Q: "P  Q  P  Q" by auto
    


subsectionImport

ML_fileIDE.ML

end