src/HOL/IsaMakefile
changeset 9346 297dcbf64526
parent 9275 5f39d82606aa
child 9353 93cd32adc402
--- a/src/HOL/IsaMakefile	Fri Jul 14 16:32:44 2000 +0200
+++ b/src/HOL/IsaMakefile	Fri Jul 14 16:32:51 2000 +0200
@@ -329,14 +329,15 @@
 HOL-MicroJava: HOL $(LOG)/HOL-MicroJava.gz
 
 $(LOG)/HOL-MicroJava.gz: $(OUT)/HOL MicroJava/ROOT.ML \
-  MicroJava/J/Conform.ML MicroJava/J/Conform.thy MicroJava/J/Decl.thy \
+  MicroJava/J/Conform.ML MicroJava/J/Conform.thy \
   MicroJava/J/Eval.thy MicroJava/J/Eval.ML MicroJava/J/JBasis.ML \
   MicroJava/J/JBasis.thy MicroJava/J/JTypeSafe.thy MicroJava/J/JTypeSafe.ML \
-  MicroJava/J/Prog.thy MicroJava/J/Prog.ML MicroJava/J/State.ML \
-  MicroJava/J/State.thy MicroJava/J/Term.thy MicroJava/J/Type.ML \
+  MicroJava/J/Decl.thy MicroJava/J/Decl.ML MicroJava/J/State.ML \
+  MicroJava/J/State.thy MicroJava/J/Term.thy \
   MicroJava/J/Type.thy MicroJava/J/TypeRel.ML MicroJava/J/TypeRel.thy \
-  MicroJava/J/WellForm.thy MicroJava/J/WellForm.ML \
+  MicroJava/J/WellForm.thy MicroJava/J/WellForm.ML MicroJava/J/Value.thy \
   MicroJava/J/WellType.ML MicroJava/J/WellType.thy \
+  MicroJava/J/Example.ML MicroJava/J/Example.thy \
   MicroJava/JVM/Control.thy MicroJava/JVM/JVMExec.thy \
   MicroJava/JVM/JVMState.thy MicroJava/JVM/LoadAndStore.thy \
   MicroJava/JVM/Method.thy MicroJava/JVM/Object.thy MicroJava/JVM/Opstack.thy \