src/HOL/IsaMakefile
changeset 8012 bbdf3c51c3b8
parent 8008 8916ea9ec178
child 8020 2823ce1753a5
     1.1 --- a/src/HOL/IsaMakefile	Thu Nov 11 12:23:45 1999 +0100
     1.2 +++ b/src/HOL/IsaMakefile	Thu Nov 11 12:24:48 1999 +0100
     1.3 @@ -294,6 +294,30 @@
     1.4  	@$(ISATOOL) usedir $(OUT)/HOL MiniML
     1.5  
     1.6  
     1.7 +## HOL-MicroJava
     1.8 +
     1.9 +HOL-MicroJava: HOL $(LOG)/HOL-MicroJava.gz
    1.10 +
    1.11 +$(LOG)/HOL-MicroJava.gz: $(OUT)/HOL \
    1.12 +  MicroJava/J/Conform.ML MicroJava/J/Conform.thy MicroJava/J/Decl.thy \
    1.13 +  MicroJava/J/Eval.thy MicroJava/J/Eval.ML MicroJava/J/JBasis.ML \
    1.14 +  MicroJava/J/JBasis.thy MicroJava/J/JTypeSafe.thy MicroJava/J/JTypeSafe.ML \
    1.15 +  MicroJava/J/Prog.thy MicroJava/J/Prog.ML MicroJava/J/State.ML \
    1.16 +  MicroJava/J/State.thy MicroJava/J/Term.thy MicroJava/J/Type.ML \
    1.17 +  MicroJava/J/Type.thy MicroJava/J/TypeRel.ML MicroJava/J/TypeRel.thy \
    1.18 +  MicroJava/J/WellForm.thy MicroJava/J/WellForm.ML \
    1.19 +  MicroJava/J/WellType.ML MicroJava/J/WellType.thy \
    1.20 +  MicroJava/JVM/Control.thy MicroJava/JVM/JVMExec.thy \
    1.21 +  MicroJava/JVM/JVMState.thy MicroJava/JVM/LoadAndStore.thy \
    1.22 +  MicroJava/JVM/Method.thy MicroJava/JVM/Method.ML \
    1.23 +  MicroJava/JVM/Object.thy MicroJava/JVM/Opstack.thy \
    1.24 +  MicroJava/JVM/Store.thy MicroJava/JVM/Store.ML \
    1.25 +  MicroJava/BV/BVSpec.thy MicroJava/BV/BVSpec.ML \
    1.26 +  MicroJava/BV/BVSpecTypeSafe.thy MicroJava/BV/BVSpecTypeSafe.ML \
    1.27 +  MicroJava/BV/Convert.thy MicroJava/BV/Convert.ML \
    1.28 +  MicroJava/BV/Correct.thy MicroJava/BV/Correct.ML
    1.29 +	@$(ISATOOL) usedir $(OUT)/HOL MicroJava
    1.30 +
    1.31  ## HOL-BCV
    1.32  
    1.33  HOL-BCV: HOL $(LOG)/HOL-BCV.gz