# HG changeset patch
# User nipkow
# Date 1319307470 -7200
# Node ID 4fbeabee6487c575fae81e161a869c76ad78d9af
# Parent  ccea94064585691193c11fd884ed5ebd2f9106fd
added isaverbatimwrite that allows to cut out snippets of thy files in their latex form and dump them in a file

diff -r ccea94064585 -r 4fbeabee6487 src/HOL/IMP/AExp.thy
--- a/src/HOL/IMP/AExp.thy	Fri Oct 21 17:39:07 2011 +0200
+++ b/src/HOL/IMP/AExp.thy	Sat Oct 22 20:17:50 2011 +0200
@@ -52,13 +52,15 @@
 
 text{* Evaluate constant subsexpressions: *}
 
+text_raw{*\begin{isaverbatimwrite}\newcommand{\AExpasimpconstdef}{% *}
 fun asimp_const :: "aexp \<Rightarrow> aexp" where
 "asimp_const (N n) = N n" |
 "asimp_const (V x) = V x" |
-"asimp_const (Plus a1 a2) =
-  (case (asimp_const a1, asimp_const a2) of
-    (N n1, N n2) \<Rightarrow> N(n1+n2) |
-    (a1',a2') \<Rightarrow> Plus a1' a2')"
+"asimp_const (Plus a\<^isub>1 a\<^isub>2) =
+  (case (asimp_const a\<^isub>1, asimp_const a\<^isub>2) of
+    (N n\<^isub>1, N n\<^isub>2) \<Rightarrow> N(n\<^isub>1+n\<^isub>2) |
+    (b\<^isub>1,b\<^isub>2) \<Rightarrow> Plus b\<^isub>1 b\<^isub>2)"
+text_raw{*}\end{isaverbatimwrite}*}
 
 theorem aval_asimp_const:
   "aval (asimp_const a) s = aval a s"
@@ -69,11 +71,13 @@
 text{* Now we also eliminate all occurrences 0 in additions. The standard
 method: optimized versions of the constructors: *}
 
+text_raw{*\begin{isaverbatimwrite}\newcommand{\AExpplusdef}{% *}
 fun plus :: "aexp \<Rightarrow> aexp \<Rightarrow> aexp" where
-"plus (N i1) (N i2) = N(i1+i2)" |
+"plus (N i\<^isub>1) (N i\<^isub>2) = N(i\<^isub>1+i\<^isub>2)" |
 "plus (N i) a = (if i=0 then a else Plus (N i) a)" |
 "plus a (N i) = (if i=0 then a else Plus a (N i))" |
-"plus a1 a2 = Plus a1 a2"
+"plus a\<^isub>1 a\<^isub>2 = Plus a\<^isub>1 a\<^isub>2"
+text_raw{*}\end{isaverbatimwrite}*}
 
 lemma aval_plus[simp]:
   "aval (plus a1 a2) s = aval a1 s + aval a2 s"
@@ -81,10 +85,12 @@
 apply simp_all (* just for a change from auto *)
 done
 
+text_raw{*\begin{isaverbatimwrite}\newcommand{\AExpasimpdef}{% *}
 fun asimp :: "aexp \<Rightarrow> aexp" where
 "asimp (N n) = N n" |
 "asimp (V x) = V x" |
-"asimp (Plus a1 a2) = plus (asimp a1) (asimp a2)"
+"asimp (Plus a\<^isub>1 a\<^isub>2) = plus (asimp a\<^isub>1) (asimp a\<^isub>2)"
+text_raw{*}\end{isaverbatimwrite}*}
 
 text{* Note that in @{const asimp_const} the optimized constructor was
 inlined. Making it a separate function @{const plus} improves modularity of
diff -r ccea94064585 -r 4fbeabee6487 src/HOL/IMP/document/isaverbatimwrite.sty
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/IMP/document/isaverbatimwrite.sty	Sat Oct 22 20:17:50 2011 +0200
@@ -0,0 +1,16 @@
+\@ifundefined{verbatim@processline}{\input verbatim.sty}{}
+
+\newwrite \isaverbatim@out
+\def\openisaverbatimout#1{\immediate\openout \isaverbatim@out #1}
+\def\closeisaverbatimout{\immediate\closeout \isaverbatim@out}
+\def\isaverbatimwrite{%
+  \@bsphack
+  \let\do\@makeother\dospecials
+  \catcode`\^^M\active \catcode`\^^I=12
+  \def\verbatim@processline{%
+    \immediate\write\isaverbatim@out
+      {\the\verbatim@line}}%
+  \verbatim@start}
+
+\def\endisaverbatimwrite{%
+  \@esphack}
diff -r ccea94064585 -r 4fbeabee6487 src/HOL/IMP/document/root.tex
--- a/src/HOL/IMP/document/root.tex	Fri Oct 21 17:39:07 2011 +0200
+++ b/src/HOL/IMP/document/root.tex	Sat Oct 22 20:17:50 2011 +0200
@@ -29,6 +29,8 @@
 % this should be the last package used
 \usepackage{pdfsetup}
 
+\usepackage{isaverbatimwrite}
+
 % urls in roman style, theory text in math-similar italics
 \urlstyle{rm}
 \isabellestyle{it}
@@ -46,6 +48,7 @@
 
 
 \begin{document}
+\openisaverbatimout fragments
 
 \title{Concrete Semantics}
 \author{TN \& GK}
diff -r ccea94064585 -r 4fbeabee6487 src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Fri Oct 21 17:39:07 2011 +0200
+++ b/src/HOL/IsaMakefile	Sat Oct 22 20:17:50 2011 +0200
@@ -531,8 +531,7 @@
   IMP/Sec_TypingT.thy IMP/Small_Step.thy IMP/Star.thy IMP/Types.thy \
   IMP/Util.thy IMP/VC.thy IMP/Vars.thy \
   IMP/ROOT.ML IMP/document/root.tex IMP/document/root.bib
-	@cd IMP && $(ISABELLE_TOOL) usedir -g true -b $(OUT)/HOL HOL-IMP
-
+	@cd IMP && $(ISABELLE_TOOL) usedir -g true -D generated -b $(OUT)/HOL HOL-IMP &&	cd generated && pdflatex root.tex
 
 ## HOL-IMPP