src/HOL/IsaMakefile
changeset 33026 8f35633c4922
parent 33024 60a098883d81
child 33027 9cf389429f6d
     1.1 --- a/src/HOL/IsaMakefile	Tue Oct 20 19:36:52 2009 +0200
     1.2 +++ b/src/HOL/IsaMakefile	Tue Oct 20 19:37:09 2009 +0200
     1.3 @@ -25,7 +25,7 @@
     1.4    HOL-IOA \
     1.5    HOL-Imperative_HOL \
     1.6    HOL-Induct \
     1.7 -  HOL-Isar_examples \
     1.8 +  HOL-Isar_Examples \
     1.9    HOL-Lambda \
    1.10    HOL-Lattice \
    1.11    HOL-Matrix \
    1.12 @@ -914,22 +914,22 @@
    1.13  	@$(ISABELLE_TOOL) usedir $(OUT)/HOL ex
    1.14  
    1.15  
    1.16 -## HOL-Isar_examples
    1.17 +## HOL-Isar_Examples
    1.18  
    1.19 -HOL-Isar_examples: HOL $(LOG)/HOL-Isar_examples.gz
    1.20 +HOL-Isar_Examples: HOL $(LOG)/HOL-Isar_Examples.gz
    1.21  
    1.22 -$(LOG)/HOL-Isar_examples.gz: $(OUT)/HOL Isar_examples/Basic_Logic.thy	\
    1.23 -  Isar_examples/Cantor.thy Isar_examples/Drinker.thy			\
    1.24 -  Isar_examples/Expr_Compiler.thy Isar_examples/Fibonacci.thy		\
    1.25 -  Isar_examples/Group.thy Isar_examples/Hoare.thy			\
    1.26 -  Isar_examples/Hoare_Ex.thy Isar_examples/Knaster_Tarski.thy		\
    1.27 -  Isar_examples/Mutilated_Checkerboard.thy				\
    1.28 -  Isar_examples/Nested_Datatype.thy Isar_examples/Peirce.thy		\
    1.29 -  Isar_examples/Puzzle.thy Isar_examples/Summation.thy			\
    1.30 -  Isar_examples/ROOT.ML Isar_examples/document/proof.sty		\
    1.31 -  Isar_examples/document/root.bib Isar_examples/document/root.tex	\
    1.32 -  Isar_examples/document/style.tex Hoare/hoare_tac.ML
    1.33 -	@$(ISABELLE_TOOL) usedir $(OUT)/HOL Isar_examples
    1.34 +$(LOG)/HOL-Isar_Examples.gz: $(OUT)/HOL Isar_Examples/Basic_Logic.thy	\
    1.35 +  Isar_Examples/Cantor.thy Isar_Examples/Drinker.thy			\
    1.36 +  Isar_Examples/Expr_Compiler.thy Isar_Examples/Fibonacci.thy		\
    1.37 +  Isar_Examples/Group.thy Isar_Examples/Hoare.thy			\
    1.38 +  Isar_Examples/Hoare_Ex.thy Isar_Examples/Knaster_Tarski.thy		\
    1.39 +  Isar_Examples/Mutilated_Checkerboard.thy				\
    1.40 +  Isar_Examples/Nested_Datatype.thy Isar_Examples/Peirce.thy		\
    1.41 +  Isar_Examples/Puzzle.thy Isar_Examples/Summation.thy			\
    1.42 +  Isar_Examples/ROOT.ML Isar_Examples/document/proof.sty		\
    1.43 +  Isar_Examples/document/root.bib Isar_Examples/document/root.tex	\
    1.44 +  Isar_Examples/document/style.tex Hoare/hoare_tac.ML
    1.45 +	@$(ISABELLE_TOOL) usedir $(OUT)/HOL Isar_Examples
    1.46  
    1.47  
    1.48  ## HOL-SET-Protocol
    1.49 @@ -1304,7 +1304,7 @@
    1.50  clean:
    1.51  	@rm -f $(OUT)/HOL-Plain $(OUT)/HOL-Main $(OUT)/HOL		\
    1.52  		$(OUT)/HOL-Nominal $(OUT)/TLA $(LOG)/HOL.gz		\
    1.53 -		$(LOG)/TLA.gz $(LOG)/HOL-Isar_examples.gz		\
    1.54 +		$(LOG)/TLA.gz $(LOG)/HOL-Isar_Examples.gz		\
    1.55  		$(LOG)/HOL-Induct.gz $(LOG)/HOL-ex.gz			\
    1.56  		$(LOG)/HOL-Subst.gz $(LOG)/HOL-IMP.gz			\
    1.57  		$(LOG)/HOL-IMPP.gz $(LOG)/HOL-Hoare.gz			\