# HG changeset patch
# User kleing
# Date 1014296889 -3600
# Node ID 2832fba717ec5e28442a25c9a0b0c360e10a27ca
# Parent  71015f46b3c1ccab05066917bb05ff0f89f242d9
new MicroJava document

diff -r 71015f46b3c1 -r 2832fba717ec src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Thu Feb 21 13:37:09 2002 +0100
+++ b/src/HOL/IsaMakefile	Thu Feb 21 14:08:09 2002 +0100
@@ -472,7 +472,8 @@
   MicroJava/BV/Effect.thy MicroJava/BV/EffectMono.thy \
   MicroJava/BV/Typing_Framework.thy MicroJava/BV/Typing_Framework_err.thy \
   MicroJava/BV/Kildall_Lift.thy \
-  MicroJava/document/root.bib MicroJava/document/root.tex
+  MicroJava/document/root.bib MicroJava/document/root.tex \
+  MicroJava/document/introduction.tex
 	@$(ISATOOL) usedir -g true $(OUT)/HOL MicroJava