src/HOL/IsaMakefile
changeset 29806 bebe5a254ba6
parent 29792 c566b63ce76a
child 29809 df25a6b1a475
     1.1 --- a/src/HOL/IsaMakefile	Wed Feb 04 18:10:07 2009 +0100
     1.2 +++ b/src/HOL/IsaMakefile	Thu Feb 05 14:14:02 2009 +0100
     1.3 @@ -311,6 +311,7 @@
     1.4  
     1.5  HOL-Library: HOL $(LOG)/HOL-Library.gz
     1.6  
     1.7 +
     1.8  $(LOG)/HOL-Library.gz: $(OUT)/HOL Library/SetsAndFunctions.thy		\
     1.9    Library/Abstract_Rat.thy \
    1.10    Library/BigO.thy Library/ContNotDenum.thy Library/Efficient_Nat.thy	\
    1.11 @@ -335,6 +336,7 @@
    1.12    Library/Mapping.thy	Library/Numeral_Type.thy	Library/Reflection.thy		\
    1.13    Library/Boolean_Algebra.thy Library/Countable.thy	\
    1.14    Library/RBT.thy	Library/Univ_Poly.thy	\
    1.15 +  Library/Random.thy	Library/Quickcheck.thy	\
    1.16    Library/Enum.thy Library/Float.thy $(SRC)/Tools/float.ML $(SRC)/HOL/Tools/float_arith.ML \
    1.17    Library/reify_data.ML Library/reflection.ML
    1.18  	@cd Library; $(ISABELLE_TOOL) usedir $(OUT)/HOL Library
    1.19 @@ -814,7 +816,7 @@
    1.20    ex/Abstract_NAT.thy ex/Antiquote.thy ex/Arith_Examples.thy ex/BT.thy	\
    1.21    ex/BinEx.thy ex/CTL.thy ex/Chinese.thy ex/Classical.thy		\
    1.22    ex/Coherent.thy ex/Dense_Linear_Order_Ex.thy ex/Eval_Examples.thy	\
    1.23 -  ex/Groebner_Examples.thy ex/Random.thy ex/Quickcheck.thy		\
    1.24 +  ex/Groebner_Examples.thy ex/Quickcheck_Generators.thy		\
    1.25    ex/Codegenerator.thy ex/Codegenerator_Pretty.thy			\
    1.26    ex/CodegenSML_Test.thy ex/Formal_Power_Series_Examples.thy						\
    1.27    ex/Commutative_RingEx.thy ex/Efficient_Nat_examples.thy		\