equal
deleted
inserted
replaced
8 theory pair imports upair |
8 theory pair imports upair |
9 uses "simpdata.ML" |
9 uses "simpdata.ML" |
10 begin |
10 begin |
11 |
11 |
12 setup {* |
12 setup {* |
13 Simplifier.map_simpset_global (fn ss => |
13 Simplifier.map_simpset_global |
14 ss setmksimps (K (map mk_eq o ZF_atomize o gen_all)) |
14 (Simplifier.set_mksimps (K (map mk_eq o ZF_atomize o gen_all)) |
15 |> Simplifier.add_cong @{thm if_weak_cong}) |
15 #> Simplifier.add_cong @{thm if_weak_cong}) |
16 *} |
16 *} |
17 |
17 |
18 ML {* val ZF_ss = @{simpset} *} |
18 ML {* val ZF_ss = @{simpset} *} |
19 |
19 |
20 simproc_setup defined_Bex ("EX x:A. P(x) & Q(x)") = {* |
20 simproc_setup defined_Bex ("EX x:A. P(x) & Q(x)") = {* |