src/FOL/simpdata.ML
changeset 745 45a789407806
parent 429 888bbb4119f8
child 756 e0e5c1581e4c
equal deleted inserted replaced
744:2054fa3c8d76 745:45a789407806
   112 fun prove_fun s = 
   112 fun prove_fun s = 
   113  (writeln s;  
   113  (writeln s;  
   114   prove_goal FOL.thy s
   114   prove_goal FOL.thy s
   115    (fn prems => [ (cut_facts_tac prems 1), 
   115    (fn prems => [ (cut_facts_tac prems 1), 
   116 		  (Cla.fast_tac FOL_cs 1) ]));
   116 		  (Cla.fast_tac FOL_cs 1) ]));
       
   117 
   117 val cla_rews = map prove_fun
   118 val cla_rews = map prove_fun
   118  ["~(P&Q)  <-> ~P | ~Q",
   119  ["~(P&Q)  <-> ~P | ~Q",
   119   "P | ~P", 		"~P | P",
   120   "P | ~P", 		"~P | P",
   120   "~ ~ P <-> P",	"(~P --> P) <-> P"];
   121   "~ ~ P <-> P",	"(~P --> P) <-> P"];
   121 
   122