src/HOL/IsaMakefile
changeset 30689 b14b2cc4e25e
parent 30654 254478a8dd05
child 30925 c38cbc0ac8d1
     1.1 --- a/src/HOL/IsaMakefile	Mon Mar 23 19:01:17 2009 +0100
     1.2 +++ b/src/HOL/IsaMakefile	Mon Mar 23 19:01:17 2009 +0100
     1.3 @@ -649,7 +649,11 @@
     1.4  $(LOG)/HOL-Imperative_HOL.gz: $(OUT)/HOL Imperative_HOL/Heap.thy \
     1.5    Imperative_HOL/Heap_Monad.thy Imperative_HOL/Array.thy \
     1.6    Imperative_HOL/Relational.thy \
     1.7 -  Imperative_HOL/Ref.thy Imperative_HOL/Imperative_HOL.thy
     1.8 +  Imperative_HOL/Ref.thy Imperative_HOL/Imperative_HOL.thy \
     1.9 +  Imperative_HOL/Imperative_HOL_ex.thy \
    1.10 +  Imperative_HOL/ex/Imperative_Quicksort.thy \
    1.11 +  Imperative_HOL/ex/Subarray.thy \
    1.12 +  Imperative_HOL/ex/Sublist.thy
    1.13  	@$(ISABELLE_TOOL) usedir $(OUT)/HOL Imperative_HOL
    1.14  
    1.15  
    1.16 @@ -836,7 +840,7 @@
    1.17    ex/Formal_Power_Series_Examples.thy ex/Fundefs.thy			\
    1.18    ex/Groebner_Examples.thy ex/Guess.thy ex/HarmonicSeries.thy		\
    1.19    ex/Hebrew.thy ex/Hex_Bin_Examples.thy ex/Higher_Order_Logic.thy	\
    1.20 -  ex/Hilbert_Classical.thy ex/ImperativeQuicksort.thy			\
    1.21 +  ex/Hilbert_Classical.thy			\
    1.22    ex/Induction_Scheme.thy ex/InductiveInvariant.thy			\
    1.23    ex/InductiveInvariant_examples.thy ex/Intuitionistic.thy		\
    1.24    ex/Lagrange.thy ex/LocaleTest2.thy ex/MT.thy ex/MergeSort.thy		\
    1.25 @@ -845,8 +849,8 @@
    1.26    ex/Quickcheck_Examples.thy ex/Quickcheck_Generators.thy ex/ROOT.ML	\
    1.27    ex/Recdefs.thy ex/Records.thy ex/ReflectionEx.thy			\
    1.28    ex/Refute_Examples.thy ex/SAT_Examples.thy ex/SVC_Oracle.thy		\
    1.29 -  ex/Serbian.thy ex/Sqrt.thy ex/Sqrt_Script.thy ex/Subarray.thy		\
    1.30 -  ex/Sublist.thy ex/Sudoku.thy ex/Tarski.thy ex/Term_Of_Syntax.thy	\
    1.31 +  ex/Serbian.thy ex/Sqrt.thy ex/Sqrt_Script.thy \
    1.32 +  ex/Sudoku.thy ex/Tarski.thy ex/Term_Of_Syntax.thy	\
    1.33    ex/Termination.thy ex/Unification.thy ex/document/root.bib		\
    1.34    ex/document/root.tex ex/set.thy ex/svc_funcs.ML ex/svc_test.thy \
    1.35    ex/Predicate_Compile.thy ex/predicate_compile.ML