src/FOL/simpdata.ML
changeset 4477 b3e5857d8d99
parent 4349 50403e5a44c0
child 4649 89ad3eb863a1
equal deleted inserted replaced
4476:fbdc87f8ac7e 4477:b3e5857d8d99
   360 fun op addsimps2 arg = pair_upd2 (op addsimps) arg;
   360 fun op addsimps2 arg = pair_upd2 (op addsimps) arg;
   361 fun op delsimps2 arg = pair_upd2 (op delsimps) arg;
   361 fun op delsimps2 arg = pair_upd2 (op delsimps) arg;
   362 fun op addcongs2 arg = pair_upd2 (op addcongs) arg;
   362 fun op addcongs2 arg = pair_upd2 (op addcongs) arg;
   363 fun op delcongs2 arg = pair_upd2 (op delcongs) arg;
   363 fun op delcongs2 arg = pair_upd2 (op delcongs) arg;
   364 
   364 
   365 fun auto_tac (cs,ss) = 
   365 
       
   366 fun mk_auto_tac (cs, ss) m n =
   366     let val cs' = cs addss ss 
   367     let val cs' = cs addss ss 
   367     in  EVERY [TRY (safe_tac cs'),
   368 	val bdt = Blast.depth_tac cs m;
   368 	       REPEAT (FIRSTGOAL (fast_tac cs')),
   369 	fun blast_depth_tac i thm = bdt i thm handle Blast.TRANS s => 
       
   370 		(warning ("Blast_tac: " ^ s); Seq.empty);
       
   371         val maintac = 
       
   372           blast_depth_tac	   (*fast but can't use addss*)
       
   373           ORELSE'
       
   374           depth_tac cs' n;         (*slower but general*)
       
   375     in  EVERY [ALLGOALS (asm_full_simp_tac ss),
       
   376 	       TRY (safe_tac cs'),
       
   377 	       REPEAT (FIRSTGOAL maintac),
   369                TRY (safe_tac (cs addSss ss)),
   378                TRY (safe_tac (cs addSss ss)),
   370 	       prune_params_tac] 
   379 	       prune_params_tac] 
   371     end;
   380     end;
   372 
   381 
   373 fun Auto_tac () = auto_tac (claset(), simpset());
   382 fun auto_tac (cs,ss) = mk_auto_tac (cs,ss) 4 2;
   374 
   383 
   375 fun auto () = by (Auto_tac ());
   384 fun Auto_tac st = auto_tac (claset(), simpset()) st;
       
   385 
       
   386 fun auto () = by Auto_tac;