merged

--- a/src/Doc/Prog_Prove/Isar.thy	Mon Oct 26 23:41:27 2015 +0000
+++ b/src/Doc/Prog_Prove/Isar.thy	Mon Oct 26 23:42:01 2015 +0000
@@ -1021,14 +1021,14 @@
 are variables. In some rare situations one needs to deal with an assumption where
 not all arguments @{text r}, @{text s}, @{text t} are variables:
 \begin{isabelle}
-\isacom{lemma} @{text[source]"I r s t \<Longrightarrow> \<dots>"}
+\isacom{lemma} @{text"\"I r s t \<Longrightarrow> \<dots>\""}
 \end{isabelle}
 Applying the standard form of
 rule induction in such a situation will lead to strange and typically unprovable goals.
 We can easily reduce this situation to the standard one by introducing
 new variables @{text x}, @{text y}, @{text z} and reformulating the goal like this:
 \begin{isabelle}
-\isacom{lemma} @{text[source]"I x y z \<Longrightarrow> x = r \<Longrightarrow> y = s \<Longrightarrow> z = t \<Longrightarrow> \<dots>"}
+\isacom{lemma} @{text"\"I x y z \<Longrightarrow> x = r \<Longrightarrow> y = s \<Longrightarrow> z = t \<Longrightarrow> \<dots>\""}
 \end{isabelle}
 Standard rule induction will work fine now, provided the free variables in
 @{text r}, @{text s}, @{text t} are generalized via @{text"arbitrary"}.
@@ -1036,7 +1036,7 @@
 However, induction can do the above transformation for us, behind the curtains, so we never
 need to see the expanded version of the lemma. This is what we need to write:
 \begin{isabelle}
-\isacom{lemma} @{text[source]"I r s t \<Longrightarrow> \<dots>"}\isanewline
+\isacom{lemma} @{text"\"I r s t \<Longrightarrow> \<dots>\""}\isanewline
 \isacom{proof}@{text"(induction \"r\" \"s\" \"t\" arbitrary: \<dots> rule: I.induct)"}\index{inductionrule@@{text"induction ... rule:"}}\index{arbitrary@@{text"arbitrary:"}}
 \end{isabelle}
 Like for rule inversion, cases that are impossible because of constructor clashes

--- a/src/Pure/Thy/latex.ML	Mon Oct 26 23:41:27 2015 +0000
+++ b/src/Pure/Thy/latex.ML	Mon Oct 26 23:42:01 2015 +0000
@@ -159,7 +159,7 @@
 (* theory presentation *)
 
 fun environment name =
-  enclose ("%\n\\begin{" ^ name ^ "}%\n") ("%\n\\end{" ^ name ^ "}%\n");
+  enclose ("%\n\\begin{" ^ name ^ "}%\n") ("%\n\\end{" ^ name ^ "}");
 
 val tex_trailer =
   "%%% Local Variables:\n\