src/FOL/IFOL.thy
changeset 18481 b75ce99617c7
parent 17702 ea88ddeafabe
child 18523 9446cb8e1f65
equal deleted inserted replaced
18480:8ac97f71369d 18481:b75ce99617c7
   140 
   140 
   141 
   141 
   142 subsection {* Lemmas and proof tools *}
   142 subsection {* Lemmas and proof tools *}
   143 
   143 
   144 use "IFOL_lemmas.ML"
   144 use "IFOL_lemmas.ML"
       
   145 
       
   146 ML {*
       
   147 structure ProjectRule = ProjectRuleFun
       
   148 (struct
       
   149   val conjunct1 = thm "conjunct1";
       
   150   val conjunct2 = thm "conjunct2";
       
   151   val mp = thm "mp";
       
   152 end)
       
   153 *}
   145 
   154 
   146 use "fologic.ML"
   155 use "fologic.ML"
   147 use "hypsubstdata.ML"
   156 use "hypsubstdata.ML"
   148 setup hypsubst_setup
   157 setup hypsubst_setup
   149 use "intprover.ML"
   158 use "intprover.ML"