equal
deleted
inserted
replaced
10 begin |
10 begin |
11 |
11 |
12 setup {* |
12 setup {* |
13 Simplifier.map_simpset_global (fn ss => |
13 Simplifier.map_simpset_global (fn ss => |
14 ss setmksimps (K (map mk_eq o ZF_atomize o gen_all)) |
14 ss setmksimps (K (map mk_eq o ZF_atomize o gen_all)) |
15 addcongs [@{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)") = {* |