# HG changeset patch
# User wenzelm
# Date 949697157 -3600
# Node ID 33e4ec7a2daa76e6aa1e72d63a88460e1511233a
# Parent  45a7027136e363f6a86a0a78a8f54cd1fc2db295
added MicroJava/document;

diff -r 45a7027136e3 -r 33e4ec7a2daa src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Fri Feb 04 21:44:38 2000 +0100
+++ b/src/HOL/IsaMakefile	Fri Feb 04 21:45:57 2000 +0100
@@ -325,9 +325,10 @@
   MicroJava/BV/BVSpec.thy MicroJava/BV/BVSpec.ML \
   MicroJava/BV/BVSpecTypeSafe.thy MicroJava/BV/BVSpecTypeSafe.ML \
   MicroJava/BV/Convert.thy MicroJava/BV/Convert.ML \
-  MicroJava/BV/Correct.thy MicroJava/BV/Correct.ML
+  MicroJava/BV/Correct.thy MicroJava/BV/Correct.ML MicroJava/document/root.tex
 	@$(ISATOOL) usedir $(OUT)/HOL MicroJava
 
+
 ## HOL-BCV
 
 HOL-BCV: HOL $(LOG)/HOL-BCV.gz
diff -r 45a7027136e3 -r 33e4ec7a2daa src/HOL/MicroJava/document/root.tex
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/MicroJava/document/root.tex	Fri Feb 04 21:45:57 2000 +0100
@@ -0,0 +1,8 @@
+
+\documentclass[11pt,a4paper]{article}
+\usepackage{isabelle,isabellesym,pdfsetup}
+
+\begin{document}
+\input{session}
+\end{document}
+