equal
deleted
inserted
replaced
258 val loop_tac = FIRST' (map (fn (_, tac) => tac ss) (rev loop_tacs)); |
258 val loop_tac = FIRST' (map (fn (_, tac) => tac ss) (rev loop_tacs)); |
259 val solve_tac = FIRST' (map (MetaSimplifier.solver ss) |
259 val solve_tac = FIRST' (map (MetaSimplifier.solver ss) |
260 (rev (if safe then solvers else unsafe_solvers))); |
260 (rev (if safe then solvers else unsafe_solvers))); |
261 |
261 |
262 fun simp_loop_tac i = |
262 fun simp_loop_tac i = |
263 Goal.asm_rewrite_goal_tac mode (solve_all_tac unsafe_solvers) ss i THEN |
263 asm_rewrite_goal_tac mode (solve_all_tac unsafe_solvers) ss i THEN |
264 (solve_tac i ORELSE TRY ((loop_tac THEN_ALL_NEW simp_loop_tac) i)); |
264 (solve_tac i ORELSE TRY ((loop_tac THEN_ALL_NEW simp_loop_tac) i)); |
265 in simp_loop_tac end; |
265 in simp_loop_tac end; |
266 |
266 |
267 local |
267 local |
268 |
268 |