src/HOL/IsaMakefile
changeset 29788 1b80ebe713a4
parent 29708 e40b70d38909
child 29792 c566b63ce76a
     1.1 --- a/src/HOL/IsaMakefile	Tue Feb 03 16:50:40 2009 +0100
     1.2 +++ b/src/HOL/IsaMakefile	Tue Feb 03 16:50:41 2009 +0100
     1.3 @@ -36,6 +36,7 @@
     1.4    HOL-Nominal-Examples \
     1.5    HOL-NumberTheory \
     1.6    HOL-Prolog \
     1.7 +  HOL-Reflection \
     1.8    HOL-SET-Protocol \
     1.9    HOL-SizeChange \
    1.10    HOL-Statespace \
    1.11 @@ -678,6 +679,21 @@
    1.12  	@$(ISABELLE_TOOL) usedir $(OUT)/HOL Prolog
    1.13  
    1.14  
    1.15 +## HOL-Reflection
    1.16 +
    1.17 +HOL-Reflection: HOL $(LOG)/HOL-Reflection.gz
    1.18 +
    1.19 +$(LOG)/HOL-Reflection.gz: $(OUT)/HOL \
    1.20 +  Reflection/Cooper.thy \
    1.21 +  Reflection/cooper_tac.ML \
    1.22 +  Reflection/Ferrack.thy \
    1.23 +  Reflection/ferrack_tac.ML \
    1.24 +  Reflection/MIR.thy \
    1.25 +  Reflection/mir_tac.ML \
    1.26 +  Reflection/ROOT.ML
    1.27 +	@$(ISABELLE_TOOL) usedir $(OUT)/HOL Reflection
    1.28 +
    1.29 +
    1.30  ## HOL-W0
    1.31  
    1.32  HOL-W0: HOL $(LOG)/HOL-W0.gz
    1.33 @@ -812,7 +828,6 @@
    1.34    ex/Numeral.thy ex/PER.thy ex/PresburgerEx.thy ex/Primrec.thy		\
    1.35    ex/Quickcheck_Examples.thy	\
    1.36    ex/ReflectionEx.thy ex/ROOT.ML ex/Recdefs.thy ex/Records.thy		\
    1.37 -  ex/Reflected_Presburger.thy ex/coopertac.ML				\
    1.38    ex/Refute_Examples.thy ex/SAT_Examples.thy ex/SVC_Oracle.thy		\
    1.39    ex/Subarray.thy ex/Sublist.thy                                        \
    1.40    ex/Sudoku.thy ex/Tarski.thy ex/Termination.thy ex/Term_Of_Syntax.thy	\
    1.41 @@ -822,10 +837,7 @@
    1.42    ex/ImperativeQuicksort.thy	\
    1.43    ex/BigO_Complex.thy			\
    1.44    ex/Arithmetic_Series_Complex.thy ex/HarmonicSeries.thy	\
    1.45 -  ex/Sqrt.thy							\
    1.46 -  ex/Sqrt_Script.thy ex/MIR.thy ex/mirtac.ML	\
    1.47 -  ex/ReflectedFerrack.thy					\
    1.48 -  ex/linrtac.ML
    1.49 +  ex/Sqrt.thy ex/Sqrt_Script.thy
    1.50  	@$(ISABELLE_TOOL) usedir $(OUT)/HOL ex
    1.51  
    1.52