src/HOL/IsaMakefile
changeset 13585 db4005b40cc6
parent 13579 57c12adaec85
child 13588 07b66a557487
     1.1 --- a/src/HOL/IsaMakefile	Thu Sep 26 10:43:43 2002 +0200
     1.2 +++ b/src/HOL/IsaMakefile	Thu Sep 26 10:51:29 2002 +0200
     1.3 @@ -83,7 +83,7 @@
     1.4    $(SRC)/TFL/usyntax.ML $(SRC)/TFL/utils.ML \
     1.5    Datatype.thy Datatype_Universe.ML Datatype_Universe.thy Divides_lemmas.ML \
     1.6    Divides.thy Extraction.thy Finite_Set.ML Finite_Set.thy \
     1.7 -  Fun.ML Fun.thy Gfp.ML Gfp.thy \
     1.8 +  Fun.thy Gfp.ML Gfp.thy \
     1.9    Hilbert_Choice.thy Hilbert_Choice_lemmas.ML HOL.ML \
    1.10    HOL.thy HOL_lemmas.ML Inductive.thy Integ/Bin.ML Integ/Bin.thy \
    1.11    Integ/Equiv.ML Integ/Equiv.thy Integ/int.ML Integ/Int.thy \
    1.12 @@ -197,7 +197,8 @@
    1.13  HOL-Library: HOL $(LOG)/HOL-Library.gz
    1.14  
    1.15  $(LOG)/HOL-Library.gz: $(OUT)/HOL Library/Accessible_Part.thy \
    1.16 -  Library/Library.thy Library/List_Prefix.thy Library/Multiset.thy \
    1.17 +  Library/FuncSet.thy Library/Library.thy \
    1.18 +  Library/List_Prefix.thy Library/Multiset.thy \
    1.19    Library/Permutation.thy Library/Primes.thy \
    1.20    Library/Quotient.thy Library/Ring_and_Field.thy \
    1.21    Library/Ring_and_Field_Example.thy Library/Nat_Infinity.thy \
    1.22 @@ -275,20 +276,16 @@
    1.23  HOL-GroupTheory: HOL $(LOG)/HOL-GroupTheory.gz
    1.24  
    1.25  $(LOG)/HOL-GroupTheory.gz: $(OUT)/HOL \
    1.26 -  Library/Primes.thy \
    1.27 -  GroupTheory/Bij.thy GroupTheory/Bij.ML\
    1.28 -  GroupTheory/Coset.thy GroupTheory/Coset.ML\
    1.29 -  GroupTheory/DirProd.thy GroupTheory/DirProd.ML\
    1.30 -  GroupTheory/Exponent.thy GroupTheory/Exponent.ML\
    1.31 -  GroupTheory/FactGroup.thy GroupTheory/FactGroup.ML\
    1.32 -  GroupTheory/Group.thy GroupTheory/Group.ML\
    1.33 -  GroupTheory/Homomorphism.thy GroupTheory/Homomorphism.ML\
    1.34 -  GroupTheory/PiSets.ML GroupTheory/PiSets.thy \
    1.35 -  GroupTheory/Ring.thy GroupTheory/Ring.ML\
    1.36 -  GroupTheory/RingConstr.thy GroupTheory/RingConstr.ML\
    1.37 -  GroupTheory/Sylow.thy GroupTheory/Sylow.ML\
    1.38 -  GroupTheory/ROOT.ML
    1.39 -	@$(ISATOOL) usedir $(OUT)/HOL GroupTheory
    1.40 +  Library/Primes.thy Library/FuncSet.thy \
    1.41 +  GroupTheory/Bij.thy \
    1.42 +  GroupTheory/Coset.thy \
    1.43 +  GroupTheory/Exponent.thy \
    1.44 +  GroupTheory/Group.thy \
    1.45 +  GroupTheory/Ring.thy \
    1.46 +  GroupTheory/Sylow.thy \
    1.47 +  GroupTheory/ROOT.ML \
    1.48 +  GroupTheory/document/root.tex
    1.49 +	@$(ISATOOL) usedir -g true $(OUT)/HOL GroupTheory
    1.50  
    1.51  
    1.52  ## HOL-Hoare