equal
deleted
inserted
replaced
110 (HOLogic.mk_Trueprop (HOLogic.mk_eq tu)) |
110 (HOLogic.mk_Trueprop (HOLogic.mk_eq tu)) |
111 (K (EVERY [expand_tac, norm_tac ss])))); |
111 (K (EVERY [expand_tac, norm_tac ss])))); |
112 |
112 |
113 fun simp_all_tac rules = |
113 fun simp_all_tac rules = |
114 let val ss0 = HOL_ss addsimps rules |
114 let val ss0 = HOL_ss addsimps rules |
115 in fn ss => ALLGOALS (simp_tac (Simplifier.inherit_context ss ss0)) end; |
115 val safe_simp_tac = generic_simp_tac true (false, false, false) |
|
116 in fn ss => ALLGOALS (safe_simp_tac (Simplifier.inherit_context ss ss0)) end; |
116 |
117 |
117 fun simplify_meta_eq rules = |
118 fun simplify_meta_eq rules = |
118 let val ss0 = HOL_basic_ss addsimps rules |> Simplifier.add_eqcong @{thm eq_cong2} |
119 let val ss0 = HOL_basic_ss addsimps rules |> Simplifier.add_eqcong @{thm eq_cong2} |
119 in fn ss => simplify (Simplifier.inherit_context ss ss0) o mk_meta_eq end |
120 in fn ss => simplify (Simplifier.inherit_context ss ss0) o mk_meta_eq end |
120 |
121 |