equal
deleted
inserted
replaced
21 FILES = ROOT.ML zf.thy zf.ML upair.ML subset.ML pair.ML domrange.ML \ |
21 FILES = ROOT.ML zf.thy zf.ML upair.ML subset.ML pair.ML domrange.ML \ |
22 func.ML simpdata.ML bool.thy bool.ML \ |
22 func.ML simpdata.ML bool.thy bool.ML \ |
23 sum.thy sum.ML qpair.thy qpair.ML mono.ML fixedpt.thy fixedpt.ML \ |
23 sum.thy sum.ML qpair.thy qpair.ML mono.ML fixedpt.thy fixedpt.ML \ |
24 ind-syntax.ML intr-elim.ML indrule.ML inductive.ML co-inductive.ML \ |
24 ind-syntax.ML intr-elim.ML indrule.ML inductive.ML co-inductive.ML \ |
25 equalities.ML perm.thy perm.ML trancl.thy trancl.ML \ |
25 equalities.ML perm.thy perm.ML trancl.thy trancl.ML \ |
26 wf.thy wf.ML ordinal.thy ordinal.ML nat.thy nat.ML \ |
26 wf.thy wf.ML ordinal.thy ord.ML nat.thy nat.ML \ |
27 epsilon.thy epsilon.ML arith.thy arith.ML univ.thy univ.ML \ |
27 epsilon.thy epsilon.ML arith.thy arith.ML univ.thy univ.ML \ |
28 quniv.thy quniv.ML constructor.ML datatype.ML \ |
28 quniv.thy quniv.ML constructor.ML datatype.ML \ |
29 fin.ML list.ML listfn.thy listfn.ML |
29 fin.ML list.ML listfn.thy listfn.ML |
30 |
30 |
31 #Uses cp rather than make_database because Poly/ML allows only 3 levels |
31 #Uses cp rather than make_database because Poly/ML allows only 3 levels |