src/HOL/IsaMakefile
changeset 6445 931fc1daa8b1
parent 6440 7c59a55bae94
child 6472 ea01eda59c07
     1.1 --- a/src/HOL/IsaMakefile	Fri Apr 16 17:44:29 1999 +0200
     1.2 +++ b/src/HOL/IsaMakefile	Fri Apr 16 17:46:02 1999 +0200
     1.3 @@ -11,7 +11,9 @@
     1.4  test: HOL-Subst HOL-Induct HOL-IMP HOL-Hoare HOL-Lex HOL-Real \
     1.5    HOL-Auth HOL-UNITY HOL-Modelcheck HOL-Lambda HOL-W0 HOL-MiniML HOL-IOA \
     1.6    HOL-AxClasses HOL-AxClasses-Group HOL-AxClasses-Lattice \
     1.7 -  HOL-AxClasses-Tutorial HOL-Quot HOL-ex TLA-Inc TLA-Buffer TLA-Memory
     1.8 +  HOL-AxClasses-Tutorial HOL-Quot HOL-ex HOL-Isar_examples TLA-Inc \
     1.9 +  TLA-Buffer TLA-Memory
    1.10 +
    1.11  all: images test
    1.12  
    1.13  
    1.14 @@ -312,6 +314,16 @@
    1.15  	@$(ISATOOL) usedir $(OUT)/HOL ex
    1.16  
    1.17  
    1.18 +## HOL-Isar_examples
    1.19 +
    1.20 +HOL-Isar_examples: HOL $(LOG)/HOL-Isar_examples.gz
    1.21 +
    1.22 +$(LOG)/HOL-Isar_examples.gz: $(OUT)/HOL Isar_examples/BasicLogic.thy \
    1.23 +  Isar_examples/Cantor.thy Isar_examples/ExprCompiler.thy \
    1.24 +  Isar_examples/Peirce.thy Isar_examples/ROOT.ML
    1.25 +	@$(ISATOOL) usedir $(OUT)/HOL Isar_examples
    1.26 +
    1.27 +
    1.28  ## TLA
    1.29  
    1.30  TLA: HOL $(OUT)/TLA
    1.31 @@ -367,5 +379,6 @@
    1.32  	  $(LOG)/HOL-MiniML.gz $(LOG)/HOL-IOA.gz $(LOG)/HOL-AxClasses.gz \
    1.33  	  $(LOG)/HOL-AxClasses-Group.gz $(LOG)/HOL-AxClasses-Lattice.gz \
    1.34  	  $(LOG)/HOL-AxClasses-Tutorial.gz $(LOG)/HOL-Quot.gz \
    1.35 -	  $(LOG)/HOL-ex.gz $(OUT)/TLA $(LOG)/TLA.gz $(LOG)/TLA-Inc.gz \
    1.36 -	  $(LOG)/TLA-Buffer.gz $(LOG)/TLA-Memory.gz
    1.37 +	  $(LOG)/HOL-ex.gz $(LOG)/HOL-Isar_examples.gz $(OUT)/TLA \
    1.38 +	  $(LOG)/TLA.gz $(LOG)/TLA-Inc.gz $(LOG)/TLA-Buffer.gz \
    1.39 +	  $(LOG)/TLA-Memory.gz