equal
deleted
inserted
replaced
7 |
7 |
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 declaration {* |
12 setup {* |
13 fn _ => Simplifier.map_ss (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 addcongs [@{thm if_weak_cong}]) |
16 *} |
16 *} |
17 |
17 |
18 ML {* val ZF_ss = @{simpset} *} |
18 ML {* val ZF_ss = @{simpset} *} |