36 Order.ML Order.thy OrderArith.ML \ |
36 Order.ML Order.thy OrderArith.ML \ |
37 OrderArith.thy OrderType.ML OrderType.thy Ordinal.ML Ordinal.thy \ |
37 OrderArith.thy OrderType.ML OrderType.thy Ordinal.ML Ordinal.thy \ |
38 Perm.ML Perm.thy QPair.ML QPair.thy QUniv.ML QUniv.thy ROOT.ML Rel.ML \ |
38 Perm.ML Perm.thy QPair.ML QPair.thy QUniv.ML QUniv.thy ROOT.ML Rel.ML \ |
39 Rel.thy Sum.ML Sum.thy Trancl.ML Trancl.thy \ |
39 Rel.thy Sum.ML Sum.thy Trancl.ML Trancl.thy \ |
40 Update.ML Update.thy Univ.ML Univ.thy WF.ML WF.thy \ |
40 Update.ML Update.thy Univ.ML Univ.thy WF.ML WF.thy \ |
41 ZF.ML ZF.thy Zorn.ML Zorn.thy add_ind_def.ML add_ind_def.thy \ |
41 ZF.ML ZF.thy Zorn.ML Zorn.thy domrange.ML \ |
42 cartprod.ML cartprod.thy constructor.ML constructor.thy domrange.ML \ |
|
43 domrange.thy equalities.ML equalities.thy func.ML func.thy \ |
42 domrange.thy equalities.ML equalities.thy func.ML func.thy \ |
44 ind_syntax.ML ind_syntax.thy indrule.ML indrule.thy intr_elim.ML \ |
43 ind_syntax.ML mono.ML mono.thy pair.ML pair.thy simpdata.ML subset.ML \ |
45 intr_elim.thy mono.ML mono.thy pair.ML pair.thy simpdata.ML subset.ML \ |
44 subset.thy thy_syntax.ML upair.ML upair.thy \ |
46 subset.thy thy_syntax.ML typechk.ML upair.ML upair.thy \ |
45 Tools/cartprod.ML Tools/datatype_package.ML Tools/inductive_package.ML \ |
|
46 Tools/primrec_package.ML Tools/typechk.ML \ |
47 Integ/EquivClass.ML Integ/EquivClass.thy Integ/Int.ML Integ/Int.thy \ |
47 Integ/EquivClass.ML Integ/EquivClass.thy Integ/Int.ML Integ/Int.thy \ |
48 Integ/twos_compl.ML Integ/Bin.ML Integ/Bin.thy |
48 Integ/twos_compl.ML Integ/Bin.ML Integ/Bin.thy |
49 @$(ISATOOL) usedir -b $(OUT)/FOL ZF |
49 @$(ISATOOL) usedir -b $(OUT)/FOL ZF |
50 |
50 |
51 |
51 |
94 |
94 |
95 $(LOG)/ZF-Resid.gz: $(OUT)/ZF Resid/Confluence.ML Resid/Confluence.thy \ |
95 $(LOG)/ZF-Resid.gz: $(OUT)/ZF Resid/Confluence.ML Resid/Confluence.thy \ |
96 Resid/Conversion.ML Resid/Conversion.thy Resid/Cube.ML Resid/Cube.thy \ |
96 Resid/Conversion.ML Resid/Conversion.thy Resid/Cube.ML Resid/Cube.thy \ |
97 Resid/ROOT.ML Resid/Redex.ML Resid/Redex.thy Resid/Reduction.ML \ |
97 Resid/ROOT.ML Resid/Redex.ML Resid/Redex.thy Resid/Reduction.ML \ |
98 Resid/Reduction.thy Resid/Residuals.ML Resid/Residuals.thy \ |
98 Resid/Reduction.thy Resid/Residuals.ML Resid/Residuals.thy \ |
99 Resid/SubUnion.ML Resid/SubUnion.thy Resid/Substitution.ML \ |
99 Resid/Substitution.ML \ |
100 Resid/Substitution.thy Resid/Terms.ML Resid/Terms.thy |
100 Resid/Substitution.thy Resid/Terms.ML Resid/Terms.thy |
101 @$(ISATOOL) usedir $(OUT)/ZF Resid |
101 @$(ISATOOL) usedir $(OUT)/ZF Resid |
102 |
102 |
103 |
103 |
104 ## ZF-ex |
104 ## ZF-ex |
109 ex/BinEx.ML ex/Brouwer.ML ex/Brouwer.thy ex/CoUnit.ML \ |
109 ex/BinEx.ML ex/Brouwer.ML ex/Brouwer.thy ex/CoUnit.ML \ |
110 ex/CoUnit.thy ex/Comb.ML ex/Comb.thy ex/Data.ML ex/Data.thy ex/Enum.ML \ |
110 ex/CoUnit.thy ex/Comb.ML ex/Comb.thy ex/Data.ML ex/Data.thy ex/Enum.ML \ |
111 ex/Enum.thy ex/LList.ML ex/LList.thy \ |
111 ex/Enum.thy ex/LList.ML ex/LList.thy \ |
112 ex/Limit.ML ex/Limit.thy ex/ListN.ML ex/ListN.thy ex/Mutil.ML \ |
112 ex/Limit.ML ex/Limit.thy ex/ListN.ML ex/ListN.thy ex/Mutil.ML \ |
113 ex/Mutil.thy ex/Ntree.ML ex/Ntree.thy ex/Primes.ML ex/Primes.thy \ |
113 ex/Mutil.thy ex/Ntree.ML ex/Ntree.thy ex/Primes.ML ex/Primes.thy \ |
|
114 ex/Primrec_defs.ML ex/Primrec_defs.thy \ |
114 ex/Primrec.ML ex/Primrec.thy ex/PropLog.ML ex/PropLog.thy ex/ROOT.ML \ |
115 ex/Primrec.ML ex/Primrec.thy ex/PropLog.ML ex/PropLog.thy ex/ROOT.ML \ |
115 ex/Ramsey.ML ex/Ramsey.thy ex/Rmap.ML ex/Rmap.thy ex/TF.ML ex/TF.thy \ |
116 ex/Ramsey.ML ex/Ramsey.thy ex/Rmap.ML ex/Rmap.thy ex/TF.ML ex/TF.thy \ |
116 ex/Term.ML ex/Term.thy ex/misc.ML |
117 ex/Term.ML ex/Term.thy ex/misc.ML |
117 @$(ISATOOL) usedir $(OUT)/ZF ex |
118 @$(ISATOOL) usedir $(OUT)/ZF ex |
118 |
119 |