src/ZF/pair.thy
changeset 16417 9bc16273c2d4
parent 14864 419b45cdb400
child 17001 51ff2bc32774
     1.1 --- a/src/ZF/pair.thy	Fri Jun 17 11:35:35 2005 +0200
     1.2 +++ b/src/ZF/pair.thy	Fri Jun 17 16:12:49 2005 +0200
     1.3 @@ -7,8 +7,8 @@
     1.4  
     1.5  header{*Ordered Pairs*}
     1.6  
     1.7 -theory pair = upair
     1.8 -files "simpdata.ML":
     1.9 +theory pair imports upair
    1.10 +uses "simpdata.ML" begin
    1.11  
    1.12  (** Lemmas for showing that <a,b> uniquely determines a and b **)
    1.13