diff -r 929659a46ecf -r 4398f0f12579 src/HOL/Bali/DefiniteAssignmentCorrect.thy
--- a/src/HOL/Bali/DefiniteAssignmentCorrect.thy	Fri Nov 25 18:58:34 2005 +0100
+++ b/src/HOL/Bali/DefiniteAssignmentCorrect.thy	Fri Nov 25 18:58:35 2005 +0100
@@ -2829,10 +2829,6 @@
       ultimately show ?thesis by (intro conjI)
     qed
   next
--- {* 
-\par
-*} (* dummy text command to break paragraph for latex;
-              large paragraphs exhaust memory of debian pdflatex *)
     case (If b c1 c2 e s0 s1 s2 Env T A)
     have G: "prg Env = G" .
     with If.hyps have eval_e: "prg Env \<turnstile>Norm s0 \<midarrow>e-\<succ>b\<rightarrow> s1" by simp
@@ -2937,10 +2933,6 @@
       ultimately show ?thesis by simp
     qed
   next
--- {* 
-\par
-*} (* dummy text command to break paragraph for latex;
-              large paragraphs exhaust memory of debian pdflatex *)
     case (Loop b c e l s0 s1 s2 s3 Env T A)
     have G: "prg Env = G" .
     with Loop.hyps have eval_e: "prg Env\<turnstile>Norm s0 \<midarrow>e-\<succ>b\<rightarrow> s1" 
@@ -3324,10 +3316,6 @@
       qed
     qed
   next
--- {* 
-\par
-*} (* dummy text command to break paragraph for latex;
-              large paragraphs exhaust memory of debian pdflatex *)
     case (Fin c1 c2 s0 s1 s2 s3 x1 Env T A)
     have G: "prg Env = G" .
     from Fin.prems obtain C1 C2 where 
@@ -3583,10 +3571,6 @@
       by simp_all      
     ultimately show ?case by (intro conjI)
   next
--- {* 
-\par
-*} (* dummy text command to break paragraph for latex;
-              large paragraphs exhaust memory of debian pdflatex *)
     case (NewA elT a e i s0 s1 s2 s3 Env T A) 
     have G: "prg Env = G" .
     from NewA.prems obtain
@@ -3888,10 +3872,6 @@
       by simp_all
     ultimately show ?case by (intro conjI) 
   next
--- {* 
-\par
-*} (* dummy text command to break paragraph for latex;
-              large paragraphs exhaust memory of debian pdflatex *)
     case (Super s Env T A)
     from Super.prems
     have "nrm A = dom (locals (store ((Norm s)::state)))"
@@ -4042,10 +4022,6 @@
       by simp_all
     ultimately show ?case by (intro conjI)
   next
--- {* 
-\par
-*} (* dummy text command to break paragraph for latex;
-              large paragraphs exhaust memory of debian pdflatex *)
     case (Cond b e0 e1 e2 s0 s1 s2 v Env T A)
     have G: "prg Env = G" .
     have "?NormalAssigned s2 A"
@@ -4282,10 +4258,6 @@
       by simp_all
     ultimately show ?case by (intro conjI)
   next
--- {* 
-\par
-*} (* dummy text command to break paragraph for latex;
-              large paragraphs exhaust memory of debian pdflatex *)
     case (LVar s vn Env T A)
     from LVar.prems
     have "nrm A = dom (locals (store ((Norm s)::state)))"