equal
deleted
inserted
replaced
111 | _ => [thm] |
111 | _ => [thm] |
112 end; |
112 end; |
113 in atoms end; |
113 in atoms end; |
114 |
114 |
115 fun mksimps pairs ctxt = |
115 fun mksimps pairs ctxt = |
116 map_filter (try mk_eq) o mk_atomize ctxt pairs o gen_all; |
116 map_filter (try mk_eq) o mk_atomize ctxt pairs o Drule.gen_all (Variable.maxidx_of ctxt); |
117 |
117 |
118 val simp_legacy_precond = |
118 val simp_legacy_precond = |
119 Attrib.setup_config_bool @{binding "simp_legacy_precond"} (K false) |
119 Attrib.setup_config_bool @{binding "simp_legacy_precond"} (K false) |
120 |
120 |
121 fun unsafe_solver_tac ctxt = |
121 fun unsafe_solver_tac ctxt = |