src/HOL/IsaMakefile
changeset 35222 4f1fba00f66d
parent 35151 117247018b54
child 35249 7024a8a8f36a
     1.1 --- a/src/HOL/IsaMakefile	Fri Feb 19 09:35:18 2010 +0100
     1.2 +++ b/src/HOL/IsaMakefile	Fri Feb 19 13:54:19 2010 +0100
     1.3 @@ -52,6 +52,7 @@
     1.4    HOL-Nominal-Examples \
     1.5    HOL-Number_Theory \
     1.6    HOL-Old_Number_Theory \
     1.7 +  HOL-Quotient_Examples \
     1.8    HOL-Probability \
     1.9    HOL-Prolog \
    1.10    HOL-Proofs-Extraction \
    1.11 @@ -265,6 +266,7 @@
    1.12    Presburger.thy \
    1.13    Predicate_Compile.thy \
    1.14    Quickcheck.thy \
    1.15 +  Quotient.thy \
    1.16    Random.thy \
    1.17    Random_Sequence.thy \
    1.18    Recdef.thy \
    1.19 @@ -307,6 +309,11 @@
    1.20    Tools/Qelim/generated_cooper.ML \
    1.21    Tools/Qelim/presburger.ML \
    1.22    Tools/Qelim/qelim.ML \
    1.23 +  Tools/Quotient/quotient_def.ML \
    1.24 +  Tools/Quotient/quotient_info.ML \
    1.25 +  Tools/Quotient/quotient_tacs.ML \
    1.26 +  Tools/Quotient/quotient_term.ML \
    1.27 +  Tools/Quotient/quotient_typ.ML \
    1.28    Tools/recdef.ML \
    1.29    Tools/res_atp.ML \
    1.30    Tools/res_axioms.ML \
    1.31 @@ -407,7 +414,10 @@
    1.32    Library/Diagonalize.thy Library/RBT.thy Library/Univ_Poly.thy		\
    1.33    Library/Poly_Deriv.thy Library/Polynomial.thy Library/Preorder.thy	\
    1.34    Library/Product_plus.thy Library/Product_Vector.thy Library/Tree.thy	\
    1.35 -  Library/Enum.thy Library/Float.thy $(SRC)/Tools/float.ML		\
    1.36 +  Library/Enum.thy Library/Float.thy Library/Quotient_List.thy          \
    1.37 +  Library/Quotient_Option.thy Library/Quotient_Product.thy              \
    1.38 +  Library/Quotient_Sum.thy Library/Quotient_Syntax.thy                  \
    1.39 +  $(SRC)/Tools/float.ML                                                 \
    1.40    $(SRC)/HOL/Tools/float_arith.ML Library/positivstellensatz.ML		\
    1.41    Library/reify_data.ML Library/reflection.ML Library/LaTeXsugar.thy	\
    1.42    Library/OptionalSugar.thy Library/SML_Quickcheck.thy
    1.43 @@ -1273,6 +1283,15 @@
    1.44  	@$(ISABELLE_TOOL) usedir $(OUT)/HOL Mutabelle
    1.45  
    1.46  
    1.47 +## HOL-Quotient_Examples
    1.48 +
    1.49 +HOL-Quotient_Examples: HOL $(LOG)/HOL-Quotient_Examples.gz
    1.50 +
    1.51 +$(LOG)/HOL-Quotient_Examples.gz: $(OUT)/HOL	      			\
    1.52 +  Quotient_Examples/LarryInt.thy Quotient_Examples/LarryDatatype.thy
    1.53 +	@$(ISABELLE_TOOL) usedir $(OUT)/HOL Quotient_Examples
    1.54 +
    1.55 +
    1.56  ## clean
    1.57  
    1.58  clean: