Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/IsaMakefile
changeset 13585 db4005b40cc6
parent 13579 57c12adaec85
child 13588 07b66a557487 
--- a/src/HOL/IsaMakefile	Thu Sep 26 10:43:43 2002 +0200
+++ b/src/HOL/IsaMakefile	Thu Sep 26 10:51:29 2002 +0200
@@ -83,7 +83,7 @@
   $(SRC)/TFL/usyntax.ML $(SRC)/TFL/utils.ML \
   Datatype.thy Datatype_Universe.ML Datatype_Universe.thy Divides_lemmas.ML \
   Divides.thy Extraction.thy Finite_Set.ML Finite_Set.thy \
-  Fun.ML Fun.thy Gfp.ML Gfp.thy \
+  Fun.thy Gfp.ML Gfp.thy \
   Hilbert_Choice.thy Hilbert_Choice_lemmas.ML HOL.ML \
   HOL.thy HOL_lemmas.ML Inductive.thy Integ/Bin.ML Integ/Bin.thy \
   Integ/Equiv.ML Integ/Equiv.thy Integ/int.ML Integ/Int.thy \
@@ -197,7 +197,8 @@
 HOL-Library: HOL $(LOG)/HOL-Library.gz
 
 $(LOG)/HOL-Library.gz: $(OUT)/HOL Library/Accessible_Part.thy \
-  Library/Library.thy Library/List_Prefix.thy Library/Multiset.thy \
+  Library/FuncSet.thy Library/Library.thy \
+  Library/List_Prefix.thy Library/Multiset.thy \
   Library/Permutation.thy Library/Primes.thy \
   Library/Quotient.thy Library/Ring_and_Field.thy \
   Library/Ring_and_Field_Example.thy Library/Nat_Infinity.thy \
@@ -275,20 +276,16 @@
 HOL-GroupTheory: HOL $(LOG)/HOL-GroupTheory.gz
 
 $(LOG)/HOL-GroupTheory.gz: $(OUT)/HOL \
-  Library/Primes.thy \
-  GroupTheory/Bij.thy GroupTheory/Bij.ML\
-  GroupTheory/Coset.thy GroupTheory/Coset.ML\
-  GroupTheory/DirProd.thy GroupTheory/DirProd.ML\
-  GroupTheory/Exponent.thy GroupTheory/Exponent.ML\
-  GroupTheory/FactGroup.thy GroupTheory/FactGroup.ML\
-  GroupTheory/Group.thy GroupTheory/Group.ML\
-  GroupTheory/Homomorphism.thy GroupTheory/Homomorphism.ML\
-  GroupTheory/PiSets.ML GroupTheory/PiSets.thy \
-  GroupTheory/Ring.thy GroupTheory/Ring.ML\
-  GroupTheory/RingConstr.thy GroupTheory/RingConstr.ML\
-  GroupTheory/Sylow.thy GroupTheory/Sylow.ML\
-  GroupTheory/ROOT.ML
-	@$(ISATOOL) usedir $(OUT)/HOL GroupTheory
+  Library/Primes.thy Library/FuncSet.thy \
+  GroupTheory/Bij.thy \
+  GroupTheory/Coset.thy \
+  GroupTheory/Exponent.thy \
+  GroupTheory/Group.thy \
+  GroupTheory/Ring.thy \
+  GroupTheory/Sylow.thy \
+  GroupTheory/ROOT.ML \
+  GroupTheory/document/root.tex
+	@$(ISATOOL) usedir -g true $(OUT)/HOL GroupTheory
 
 
 ## HOL-Hoare
isabelle