src/ZF/pair.thy
changeset 48891 c0eafbd55de3
parent 46953 2b6e55924af3
child 51717 9e7d1c139569
     1.1 --- a/src/ZF/pair.thy	Wed Aug 22 22:47:16 2012 +0200
     1.2 +++ b/src/ZF/pair.thy	Wed Aug 22 22:55:41 2012 +0200
     1.3 @@ -6,9 +6,10 @@
     1.4  header{*Ordered Pairs*}
     1.5  
     1.6  theory pair imports upair
     1.7 -uses "simpdata.ML"
     1.8  begin
     1.9  
    1.10 +ML_file "simpdata.ML"
    1.11 +
    1.12  setup {*
    1.13    Simplifier.map_simpset_global
    1.14      (Simplifier.set_mksimps (K (map mk_eq o ZF_atomize o gen_all))