# HG changeset patch # User clasohm # Date 750344453 -3600 # Node ID 5c66481a7e9064a0da3b0fe6767d43110e95d9de # Parent 37e93ef9c756f6fac7a109d6c7d10278f4abbcdc renamed ordinal.ML to ord.ML diff -r 37e93ef9c756 -r 5c66481a7e90 src/ZF/Makefile --- a/src/ZF/Makefile Mon Oct 11 13:58:22 1993 +0100 +++ b/src/ZF/Makefile Mon Oct 11 14:00:53 1993 +0100 @@ -23,7 +23,7 @@ sum.thy sum.ML qpair.thy qpair.ML mono.ML fixedpt.thy fixedpt.ML \ ind-syntax.ML intr-elim.ML indrule.ML inductive.ML co-inductive.ML \ equalities.ML perm.thy perm.ML trancl.thy trancl.ML \ - wf.thy wf.ML ordinal.thy ordinal.ML nat.thy nat.ML \ + wf.thy wf.ML ordinal.thy ord.ML nat.thy nat.ML \ epsilon.thy epsilon.ML arith.thy arith.ML univ.thy univ.ML \ quniv.thy quniv.ML constructor.ML datatype.ML \ fin.ML list.ML listfn.thy listfn.ML