src/HOL/IsaMakefile
changeset 29650 cc3958d31b1d
parent 29628 d9294387ab0e
child 29686 4cd2874eb5ff
     1.1 --- a/src/HOL/IsaMakefile	Wed Jan 28 10:43:31 2009 +0100
     1.2 +++ b/src/HOL/IsaMakefile	Wed Jan 28 11:04:10 2009 +0100
     1.3 @@ -331,10 +331,11 @@
     1.4    Library/Binomial.thy Library/Eval_Witness.thy	\
     1.5    Library/Code_Index.thy Library/Code_Char.thy				\
     1.6    Library/Code_Char_chr.thy Library/Code_Integer.thy			\
     1.7 -  Library/Numeral_Type.thy			\
     1.8 +  Library/Numeral_Type.thy	Library/Reflection.thy		\
     1.9    Library/Boolean_Algebra.thy Library/Countable.thy	\
    1.10    Library/RBT.thy	Library/Univ_Poly.thy	\
    1.11 -  Library/Enum.thy Library/Float.thy $(SRC)/Tools/float.ML $(SRC)/HOL/Tools/float_arith.ML
    1.12 +  Library/Enum.thy Library/Float.thy $(SRC)/Tools/float.ML $(SRC)/HOL/Tools/float_arith.ML \
    1.13 +  Library/reify_data.ML Library/reflection.ML
    1.14  	@cd Library; $(ISABELLE_TOOL) usedir $(OUT)/HOL Library
    1.15  
    1.16  
    1.17 @@ -809,14 +810,14 @@
    1.18    ex/Lagrange.thy ex/LocaleTest2.thy ex/MT.thy		\
    1.19    ex/MergeSort.thy ex/MonoidGroup.thy ex/Multiquote.thy ex/NatSum.thy	\
    1.20    ex/Numeral.thy ex/PER.thy ex/PresburgerEx.thy ex/Primrec.thy		\
    1.21 -  ex/Quickcheck_Examples.thy ex/Reflection.thy ex/reflection_data.ML	\
    1.22 +  ex/Quickcheck_Examples.thy	\
    1.23    ex/ReflectionEx.thy ex/ROOT.ML ex/Recdefs.thy ex/Records.thy		\
    1.24    ex/Reflected_Presburger.thy ex/coopertac.ML				\
    1.25    ex/Refute_Examples.thy ex/SAT_Examples.thy ex/SVC_Oracle.thy		\
    1.26    ex/Subarray.thy ex/Sublist.thy                                        \
    1.27    ex/Sudoku.thy ex/Tarski.thy ex/Termination.thy ex/Term_Of_Syntax.thy	\
    1.28    ex/Unification.thy ex/document/root.bib			        \
    1.29 -  ex/document/root.tex ex/Meson_Test.thy ex/reflection.ML ex/set.thy	\
    1.30 +  ex/document/root.tex ex/Meson_Test.thy ex/set.thy	\
    1.31    ex/svc_funcs.ML ex/svc_test.thy	\
    1.32    ex/ImperativeQuicksort.thy	\
    1.33    ex/BigO_Complex.thy			\
    1.34 @@ -968,7 +969,7 @@
    1.35  
    1.36  HOL-Word: HOL $(OUT)/HOL-Word
    1.37  
    1.38 -$(OUT)/HOL-Word: $(OUT)/HOL Word/ROOT.ML Library/Infinite_Set.thy	\
    1.39 +$(OUT)/HOL-Word: $(OUT)/HOL Word/ROOT.ML	\
    1.40    Library/Boolean_Algebra.thy			\
    1.41    Library/Numeral_Type.thy Word/Num_Lemmas.thy Word/TdThs.thy		\
    1.42    Word/Size.thy Word/BinGeneral.thy Word/BinOperations.thy		\