equal
deleted
inserted
replaced
10 |
10 |
11 ML_file "simpdata.ML" |
11 ML_file "simpdata.ML" |
12 |
12 |
13 setup \<open> |
13 setup \<open> |
14 map_theory_simpset |
14 map_theory_simpset |
15 (Simplifier.set_mksimps (fn ctxt => |
15 (Simplifier.set_mksimps (fn ctxt => map mk_eq o ZF_atomize o Variable.gen_all ctxt) |
16 map mk_eq o ZF_atomize o Drule.gen_all (Variable.maxidx_of ctxt)) |
|
17 #> Simplifier.add_cong @{thm if_weak_cong}) |
16 #> Simplifier.add_cong @{thm if_weak_cong}) |
18 \<close> |
17 \<close> |
19 |
18 |
20 ML \<open>val ZF_ss = simpset_of @{context}\<close> |
19 ML \<open>val ZF_ss = simpset_of @{context}\<close> |
21 |
20 |