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