--- a/src/HOL/Bali/AxCompl.thy Fri Nov 25 18:58:34 2005 +0100
+++ b/src/HOL/Bali/AxCompl.thy Fri Nov 25 18:58:35 2005 +0100
@@ -1233,10 +1233,6 @@
show "G,A\<turnstile>{=:n} \<langle>Methd D mn\<rangle>\<^sub>e\<succ> {G\<rightarrow>}"
by simp
next
--- {*
-\par
-*} (* dummy text command to break paragraph for latex;
- large paragraphs exhaust memory of debian pdflatex *)
case (Body D c)
have mgf_c: "G,A\<turnstile>{=:n} \<langle>c\<rangle>\<^sub>s\<succ> {G\<rightarrow>}" .
from wf MGFn_Init [OF hyp] mgf_c
--- a/src/HOL/Bali/AxSound.thy Fri Nov 25 18:58:34 2005 +0100
+++ b/src/HOL/Bali/AxSound.thy Fri Nov 25 18:58:35 2005 +0100
@@ -569,10 +569,6 @@
qed
qed
next
--- {*
-\par
-*} (* dummy text command to break paragraph for latex;
- large paragraphs exhaust memory of debian pdflatex *)
case (AVar A P Q R e1 e2)
have valid_e1: "G,A|\<Turnstile>\<Colon>{ {Normal P} e1-\<succ> {Q} }" .
have valid_e2: "\<And> a. G,A|\<Turnstile>\<Colon>{ {Q\<leftarrow>In1 a} e2-\<succ> {\<lambda>Val:i:. avar G i a ..; R} }"
@@ -882,10 +878,6 @@
qed
qed
next
--- {*
-\par
-*} (* dummy text command to break paragraph for latex;
- large paragraphs exhaust memory of debian pdflatex *)
case (BinOp A P Q R binop e1 e2)
assume valid_e1: "G,A|\<Turnstile>\<Colon>{ {Normal P} e1-\<succ> {Q} }"
have valid_e2: "\<And> v1. G,A|\<Turnstile>\<Colon>{ {Q\<leftarrow>In1 v1}
@@ -1223,10 +1215,6 @@
qed
qed
next
--- {*
-\par
-*} (* dummy text command to break paragraph for latex;
- large paragraphs exhaust memory of debian pdflatex *)
case (Call A P Q R S accC' args e mn mode pTs' statT)
have valid_e: "G,A|\<Turnstile>\<Colon>{ {Normal P} e-\<succ> {Q} }" .
have valid_args: "\<And> a. G,A|\<Turnstile>\<Colon>{ {Q\<leftarrow>In1 a} args\<doteq>\<succ> {R a} }"
@@ -1611,10 +1599,6 @@
qed
qed
next
--- {*
-\par
-*} (* dummy text command to break paragraph for latex;
- large paragraphs exhaust memory of debian pdflatex *)
case (Methd A P Q ms)
have valid_body: "G,A \<union> {{P} Methd-\<succ> {Q} | ms}|\<Turnstile>\<Colon>{{P} body G-\<succ> {Q} | ms}".
show "G,A|\<Turnstile>\<Colon>{{P} Methd-\<succ> {Q} | ms}"
@@ -1825,10 +1809,6 @@
qed
qed
next
--- {*
-\par
-*} (* dummy text command to break paragraph for latex;
- large paragraphs exhaust memory of debian pdflatex *)
case (Lab A P Q c l)
have valid_c: "G,A|\<Turnstile>\<Colon>{ {Normal P} .c. {abupd (absorb l) .; Q} }".
show "G,A|\<Turnstile>\<Colon>{ {Normal P} .l\<bullet> c. {Q} }"
@@ -2232,10 +2212,6 @@
qed
qed
next
--- {*
-\par
-*} (* dummy text command to break paragraph for latex;
- large paragraphs exhaust memory of debian pdflatex *)
case (Jmp A P j)
show "G,A|\<Turnstile>\<Colon>{ {Normal (abupd (\<lambda>a. Some (Jump j)) .; P\<leftarrow>\<diamondsuit>)} .Jmp j. {P} }"
proof (rule valid_stmt_NormalI)
@@ -2507,10 +2483,6 @@
qed
qed
next
--- {*
-\par
-*} (* dummy text command to break paragraph for latex;
- large paragraphs exhaust memory of debian pdflatex *)
case (Done A C P)
show "G,A|\<Turnstile>\<Colon>{ {Normal (P\<leftarrow>\<diamondsuit> \<and>. initd C)} .Init C. {P} }"
proof (rule valid_stmt_NormalI)
--- 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)))"
--- 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
--- a/src/HOL/Bali/Evaln.thy Fri Nov 25 18:58:34 2005 +0100
+++ b/src/HOL/Bali/Evaln.thy Fri Nov 25 18:58:35 2005 +0100
@@ -742,10 +742,6 @@
by (rule evaln.Super)
then show ?case ..
next
--- {*
-\par
-*} (* dummy text command to break paragraph for latex;
- large paragraphs exhaust memory of debian pdflatex *)
case (Acc f s0 s1 v va)
then obtain n where
"G\<turnstile>Norm s0 \<midarrow>va=\<succ>(v, f)\<midarrow>n\<rightarrow> s1"
--- a/src/HOL/Bali/TypeSafe.thy Fri Nov 25 18:58:34 2005 +0100
+++ b/src/HOL/Bali/TypeSafe.thy Fri Nov 25 18:58:35 2005 +0100
@@ -939,11 +939,6 @@
subsection "accessibility"
-text {*
-\par
-*} (* dummy text command to break paragraph for latex;
- large paragraphs exhaust memory of debian pdflatex *)
-
theorem dynamic_field_access_ok:
assumes wf: "wf_prog G" and
not_Null: "\<not> stat \<longrightarrow> a\<noteq>Null" and
@@ -1922,10 +1917,6 @@
a boolean value is part of @{term hyp_e}. See also Loop
*}
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 L accC T A)
have eval_e: "G\<turnstile>Norm s0 \<midarrow>e-\<succ>b\<rightarrow> s1" .
have hyp_e: "PROP ?TypeSafe (Norm s0) s1 (In1l e) (In1 b)" .
@@ -2216,10 +2207,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 L accC T A)
have eval_c1: "G\<turnstile>Norm s0 \<midarrow>c1\<rightarrow> (x1, s1)" .
have eval_c2: "G\<turnstile>Norm s1 \<midarrow>c2\<rightarrow> s2" .
@@ -2498,10 +2485,6 @@
(error_free (Norm s0) = error_free s3) "
by simp
next
--- {*
-\par
-*} (* dummy text command to break paragraph for latex;
- large paragraphs exhaust memory of debian pdflatex *)
case (Cast castT e s0 s1 s2 v L accC T A)
have "G\<turnstile>Norm s0 \<midarrow>e-\<succ>v\<rightarrow> s1" .
have s2:"s2 = abupd (raise_if (\<not> G,store s1\<turnstile>v fits castT) ClassCast) s1" .
@@ -2715,10 +2698,6 @@
(error_free (Norm s) = error_free (Norm s))"
by simp
next
--- {*
-\par
-*} (* dummy text command to break paragraph for latex;
- large paragraphs exhaust memory of debian pdflatex *)
case (Acc upd s0 s1 w v L accC T A)
have hyp: "PROP ?TypeSafe (Norm s0) s1 (In2 v) (In2 (w,upd))" .
have conf_s0: "Norm s0\<Colon>\<preceq>(G, L)" .
@@ -2916,10 +2895,6 @@
qed
qed
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 L accC T A)
have eval_e0: "G\<turnstile>Norm s0 \<midarrow>e0-\<succ>b\<rightarrow> s1" .
have eval_e1_e2: "G\<turnstile>s1 \<midarrow>(if the_Bool b then e1 else e2)-\<succ>v\<rightarrow> s2" .
@@ -3357,10 +3332,6 @@
qed
qed
next
--- {*
-\par
-*} (* dummy text command to break paragraph for latex;
- large paragraphs exhaust memory of debian pdflatex *)
case (Methd D s0 s1 sig v L accC T A)
have "G\<turnstile>Norm s0 \<midarrow>body G D sig-\<succ>v\<rightarrow> s1" .
have hyp:"PROP ?TypeSafe (Norm s0) s1 (In1l (body G D sig)) (In1 v)" .
@@ -3726,10 +3697,6 @@
then show ?case
by (auto elim!: wt_elim_cases)
next
--- {*
-\par
-*} (* dummy text command to break paragraph for latex;
- large paragraphs exhaust memory of debian pdflatex *)
case (Cons e es s0 s1 s2 v vs L accC T A)
have eval_e: "G\<turnstile>Norm s0 \<midarrow>e-\<succ>v\<rightarrow> s1" .
have eval_es: "G\<turnstile>s1 \<midarrow>es\<doteq>\<succ>vs\<rightarrow> s2" .