equal
deleted
inserted
replaced
348 setSolver unsafe_solver |
348 setSolver unsafe_solver |
349 setmksimps (mksimps mksimps_pairs) |
349 setmksimps (mksimps mksimps_pairs) |
350 setmkeqTrue mk_eq_True |
350 setmkeqTrue mk_eq_True |
351 setmkcong mk_meta_cong; |
351 setmkcong mk_meta_cong; |
352 |
352 |
353 fun unfold_tac ss ths = |
353 fun unfold_tac ths = |
354 ALLGOALS (full_simp_tac |
354 let val ss0 = Simplifier.clear_ss HOL_basic_ss addsimps ths |
355 (Simplifier.inherit_context ss (Simplifier.clear_ss HOL_basic_ss) addsimps ths)); |
355 in fn ss => ALLGOALS (full_simp_tac (Simplifier.inherit_context ss ss0)) end; |
356 |
356 |
357 (*In general it seems wrong to add distributive laws by default: they |
357 (*In general it seems wrong to add distributive laws by default: they |
358 might cause exponential blow-up. But imp_disjL has been in for a while |
358 might cause exponential blow-up. But imp_disjL has been in for a while |
359 and cannot be removed without affecting existing proofs. Moreover, |
359 and cannot be removed without affecting existing proofs. Moreover, |
360 rewriting by "(P|Q --> R) = ((P-->R)&(Q-->R))" might be justified on the |
360 rewriting by "(P|Q --> R) = ((P-->R)&(Q-->R))" might be justified on the |