37 $(SRC)/TFL/dcterm.sml $(SRC)/TFL/post.sml $(SRC)/TFL/rules.new.sml \ |
37 $(SRC)/TFL/dcterm.sml $(SRC)/TFL/post.sml $(SRC)/TFL/rules.new.sml \ |
38 $(SRC)/TFL/rules.sig $(SRC)/TFL/sys.sml $(SRC)/TFL/tfl.sig \ |
38 $(SRC)/TFL/rules.sig $(SRC)/TFL/sys.sml $(SRC)/TFL/tfl.sig \ |
39 $(SRC)/TFL/tfl.sml $(SRC)/TFL/thms.sig $(SRC)/TFL/thms.sml \ |
39 $(SRC)/TFL/tfl.sml $(SRC)/TFL/thms.sig $(SRC)/TFL/thms.sml \ |
40 $(SRC)/TFL/thry.sig $(SRC)/TFL/thry.sml $(SRC)/TFL/usyntax.sig \ |
40 $(SRC)/TFL/thry.sig $(SRC)/TFL/thry.sml $(SRC)/TFL/usyntax.sig \ |
41 $(SRC)/TFL/usyntax.sml $(SRC)/TFL/utils.sig $(SRC)/TFL/utils.sml \ |
41 $(SRC)/TFL/usyntax.sml $(SRC)/TFL/utils.sig $(SRC)/TFL/utils.sml \ |
42 Arith.ML Arith.thy Divides.ML Divides.thy Finite.ML Finite.thy Fun.ML \ |
42 Arith.ML Arith.thy Datatype.thy \ |
|
43 Divides.ML Divides.thy Finite.ML Finite.thy Fun.ML \ |
43 Fun.thy Gfp.ML Gfp.thy HOL.ML HOL.thy Inductive.thy Integ/Bin.ML \ |
44 Fun.thy Gfp.ML Gfp.thy HOL.ML HOL.thy Inductive.thy Integ/Bin.ML \ |
44 Integ/Bin.thy Integ/Equiv.ML Integ/Equiv.thy Integ/Integ.ML \ |
45 Integ/Bin.thy Integ/Equiv.ML Integ/Equiv.thy Integ/Integ.ML \ |
45 Integ/Integ.thy Lfp.ML Lfp.thy List.ML List.thy Main.thy Map.ML Map.thy Nat.ML \ |
46 Integ/Integ.thy Lfp.ML Lfp.thy List.ML List.thy Main.thy Map.ML Map.thy Nat.ML \ |
46 Nat.thy NatDef.ML NatDef.thy Option.ML Option.thy Ord.ML Ord.thy \ |
47 Nat.thy NatDef.ML NatDef.thy Option.ML Option.thy Ord.ML Ord.thy \ |
47 Power.ML Power.thy Prod.ML Prod.thy ROOT.ML Recdef.thy Record.thy RelPow.ML \ |
48 Power.ML Power.thy Prod.ML Prod.thy ROOT.ML Recdef.thy Record.thy RelPow.ML \ |
48 RelPow.thy Relation.ML Relation.thy Set.ML Set.thy Sexp.ML Sexp.thy \ |
49 RelPow.thy Relation.ML Relation.thy Set.ML Set.thy Sexp.ML Sexp.thy \ |
49 String.ML String.thy Sum.ML Sum.thy Tools/inductive_package.ML Tools/record_package.ML \ |
50 String.ML String.thy Sum.ML Sum.thy \ |
|
51 Tools/datatype_aux.ML Tools/datatype_abs_proofs.ML Tools/datatype_package.ML \ |
|
52 Tools/datatype_prop.ML Tools/datatype_rep_proofs.ML \ |
|
53 Tools/inductive_package.ML Tools/primrec_package.ML Tools/record_package.ML \ |
50 Tools/typedef_package.ML Trancl.ML Trancl.thy Univ.ML Univ.thy \ |
54 Tools/typedef_package.ML Trancl.ML Trancl.thy Univ.ML Univ.thy \ |
51 Update.ML Update.thy Vimage.ML Vimage.thy WF.ML WF.thy WF_Rel.ML \ |
55 Update.ML Update.thy Vimage.ML Vimage.thy WF.ML WF.thy WF_Rel.ML \ |
52 WF_Rel.thy arith_data.ML cladata.ML datatype.ML equalities.ML \ |
56 WF_Rel.thy arith_data.ML cladata.ML equalities.ML \ |
53 equalities.thy hologic.ML mono.ML mono.thy simpdata.ML subset.ML \ |
57 equalities.thy hologic.ML mono.ML mono.thy simpdata.ML subset.ML \ |
54 subset.thy thy_data.ML thy_syntax.ML |
58 subset.thy thy_syntax.ML |
55 @$(ISATOOL) usedir -b $(OUT)/Pure HOL |
59 @$(ISATOOL) usedir -b $(OUT)/Pure HOL |
56 |
60 |
57 |
61 |
58 ## HOL-Subst |
62 ## HOL-Subst |
59 |
63 |