src/HOL/IsaMakefile
changeset 29809 df25a6b1a475
parent 29805 a5da150bd0ab
parent 29806 bebe5a254ba6
child 29813 3ccd86c214bf
     1.1 --- a/src/HOL/IsaMakefile	Thu Feb 05 11:49:15 2009 +0100
     1.2 +++ b/src/HOL/IsaMakefile	Thu Feb 05 14:50:43 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,7 +336,8 @@
    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/Enum.thy Library/Float.thy $(SRC)/Tools/float.ML \
    1.16 +  Library/Random.thy	Library/Quickcheck.thy	\
    1.17 +  Library/Enum.thy Library/Float.thy $(SRC)/Tools/float.ML $(SRC)/HOL/Tools/float_arith.ML \
    1.18    Library/reify_data.ML Library/reflection.ML
    1.19  	@cd Library; $(ISABELLE_TOOL) usedir $(OUT)/HOL Library
    1.20  
    1.21 @@ -815,7 +817,7 @@
    1.22    ex/Abstract_NAT.thy ex/Antiquote.thy ex/Arith_Examples.thy ex/BT.thy	\
    1.23    ex/BinEx.thy ex/CTL.thy ex/Chinese.thy ex/Classical.thy		\
    1.24    ex/Coherent.thy ex/Dense_Linear_Order_Ex.thy ex/Eval_Examples.thy	\
    1.25 -  ex/Groebner_Examples.thy ex/Random.thy ex/Quickcheck.thy		\
    1.26 +  ex/Groebner_Examples.thy ex/Quickcheck_Generators.thy		\
    1.27    ex/Codegenerator.thy ex/Codegenerator_Pretty.thy			\
    1.28    ex/CodegenSML_Test.thy ex/Formal_Power_Series_Examples.thy						\
    1.29    ex/Commutative_RingEx.thy ex/Efficient_Nat_examples.thy		\