--- a/src/HOL/Bali/Eval.thy Fri Nov 25 18:58:34 2005 +0100
+++ b/src/HOL/Bali/Eval.thy Fri Nov 25 18:58:35 2005 +0100
@@ -545,12 +545,6 @@
G\<turnstile>(Some (Xcpt (Std xn)),s0) \<midarrow>sxalloc\<rightarrow> (Some (Xcpt (Loc a)),s1)"
-text {*
-\par
-*} (* dummy text command to break paragraph for latex;
- large paragraphs exhaust memory of debian pdflatex *)
-
-
inductive "eval G" intros
--{* propagation of abrupt completion *}
@@ -793,11 +787,6 @@
*}
-text {*
-\par
-*} (* dummy text command to break paragraph for latex;
- large paragraphs exhaust memory of debian pdflatex *)
-
lemmas eval_induct = eval_induct_ [split_format and and and and and and and and
and and and and and and s1 (* Acc *) and and s2 (* Comp *) and and and and
and and