# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1286578158 -3600
# Node ID 3e9b4ce0aeca46302f60ff1b3838cb74bb71ecc8
# Parent  7044f796d8d1c4fd607527a9260e087b6cb12190
added apendix to paper detailing one proof

diff -r 7044f796d8d1 -r 3e9b4ce0aeca IsaMakefile
--- a/IsaMakefile	Fri Oct 08 15:37:11 2010 +0100
+++ b/IsaMakefile	Fri Oct 08 23:49:18 2010 +0100
@@ -28,6 +28,7 @@
 paper: $(LOG)/HOL-Nominal2-Paper.gz
 
 $(LOG)/HOL-Nominal2-Paper.gz: Paper/ROOT.ML Paper/document/root.* Paper/*.thy
+	@$(USEDIR) -f ROOTa.ML -D generated HOL Paper
 	@$(USEDIR) -D generated HOL Paper
 	$(ISABELLE_TOOL) document -o pdf  Paper/generated
 	@cp Paper/document.pdf paper.pdf
diff -r 7044f796d8d1 -r 3e9b4ce0aeca Paper/Paper.thy
--- a/Paper/Paper.thy	Fri Oct 08 15:37:11 2010 +0100
+++ b/Paper/Paper.thy	Fri Oct 08 23:49:18 2010 +0100
@@ -2389,8 +2389,8 @@
   also for patiently explaining some of the finer points of the work on the Ott-tool.
   %Stephanie Weirich suggested to separate the subgrammars
   %of kinds and types in our Core-Haskell example. \\[-6mm] 
+*}
 
-*}
 
 (*<*)
 end
diff -r 7044f796d8d1 -r 3e9b4ce0aeca Paper/document/root.tex
--- a/Paper/document/root.tex	Fri Oct 08 15:37:11 2010 +0100
+++ b/Paper/document/root.tex	Fri Oct 08 23:49:18 2010 +0100
@@ -97,10 +97,13 @@
 \input{session}
 
 \begin{spacing}{0.9}
-\bibliographystyle{plain}
-\bibliography{root}
+  \bibliographystyle{plain}
+  \bibliography{root}
 \end{spacing}
 
+\pagebreak
+\input{Appendix} 
+
 \end{document}
 
 %%% Local Variables: