diff -r 3d4ad560b2ff -r ac335b2f4a39 src/HOL/Bali/DefiniteAssignmentCorrect.thy
--- a/src/HOL/Bali/DefiniteAssignmentCorrect.thy	Fri Nov 01 10:35:50 2002 +0100
+++ b/src/HOL/Bali/DefiniteAssignmentCorrect.thy	Fri Nov 01 13:16:28 2002 +0100
@@ -2829,6 +2829,10 @@
       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
@@ -3325,6 +3329,10 @@
       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 
@@ -3580,6 +3588,10 @@
       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
@@ -3881,6 +3893,10 @@
       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)))"
@@ -4271,6 +4287,10 @@
       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)))"