src/FOL/simpdata.ML
changeset 18708 4b3dadb4fe33
parent 18529 540da2415751
child 20223 89d2758ecddf
equal deleted inserted replaced
18707:9d6154f76476 18708:4b3dadb4fe33
   359     "(~P <-> ~Q) <-> (P<->Q)"]);
   359     "(~P <-> ~Q) <-> (P<->Q)"]);
   360 
   360 
   361 (*classical simprules too*)
   361 (*classical simprules too*)
   362 val FOL_ss = IFOL_ss addsimps (cla_simps @ cla_ex_simps @ cla_all_simps);
   362 val FOL_ss = IFOL_ss addsimps (cla_simps @ cla_ex_simps @ cla_all_simps);
   363 
   363 
   364 val simpsetup = [fn thy => (change_simpset_of thy (fn _ => FOL_ss); thy)];
   364 val simpsetup = (fn thy => (change_simpset_of thy (fn _ => FOL_ss); thy));
   365 
   365 
   366 
   366 
   367 (*** integration of simplifier with classical reasoner ***)
   367 (*** integration of simplifier with classical reasoner ***)
   368 
   368 
   369 structure Clasimp = ClasimpFun
   369 structure Clasimp = ClasimpFun