equal
deleted
inserted
replaced
4 *) |
4 *) |
5 |
5 |
6 header{*Ordered Pairs*} |
6 header{*Ordered Pairs*} |
7 |
7 |
8 theory pair imports upair |
8 theory pair imports upair |
9 uses "simpdata.ML" |
|
10 begin |
9 begin |
|
10 |
|
11 ML_file "simpdata.ML" |
11 |
12 |
12 setup {* |
13 setup {* |
13 Simplifier.map_simpset_global |
14 Simplifier.map_simpset_global |
14 (Simplifier.set_mksimps (K (map mk_eq o ZF_atomize o gen_all)) |
15 (Simplifier.set_mksimps (K (map mk_eq o ZF_atomize o gen_all)) |
15 #> Simplifier.add_cong @{thm if_weak_cong}) |
16 #> Simplifier.add_cong @{thm if_weak_cong}) |