--- 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)))"