# HG changeset patch # User wenzelm # Date 1132941515 -3600 # Node ID 4398f0f125799a38a02a59f2b17e01ecf242456d # Parent 929659a46ecfb3dd21ff5252c2db4c24319ab591 removed obsolete dummy paragraphs; diff -r 929659a46ecf -r 4398f0f12579 src/HOL/Bali/AxCompl.thy --- 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\{=:n} \Methd D mn\\<^sub>e\ {G\}" 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\{=:n} \c\\<^sub>s\ {G\}" . from wf MGFn_Init [OF hyp] mgf_c diff -r 929659a46ecf -r 4398f0f12579 src/HOL/Bali/AxSound.thy --- 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|\\{ {Normal P} e1-\ {Q} }" . have valid_e2: "\ a. G,A|\\{ {Q\In1 a} e2-\ {\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|\\{ {Normal P} e1-\ {Q} }" have valid_e2: "\ v1. G,A|\\{ {Q\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|\\{ {Normal P} e-\ {Q} }" . have valid_args: "\ a. G,A|\\{ {Q\In1 a} args\\ {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 \ {{P} Methd-\ {Q} | ms}|\\{{P} body G-\ {Q} | ms}". show "G,A|\\{{P} Methd-\ {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|\\{ {Normal P} .c. {abupd (absorb l) .; Q} }". show "G,A|\\{ {Normal P} .l\ 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|\\{ {Normal (abupd (\a. Some (Jump j)) .; P\\)} .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|\\{ {Normal (P\\ \. initd C)} .Init C. {P} }" proof (rule valid_stmt_NormalI) 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 \Norm s0 \e-\b\ 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\Norm s0 \e-\b\ 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)))" diff -r 929659a46ecf -r 4398f0f12579 src/HOL/Bali/Eval.thy --- 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\(Some (Xcpt (Std xn)),s0) \sxalloc\ (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 diff -r 929659a46ecf -r 4398f0f12579 src/HOL/Bali/Evaln.thy --- 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\Norm s0 \va=\(v, f)\n\ s1" diff -r 929659a46ecf -r 4398f0f12579 src/HOL/Bali/TypeSafe.thy --- 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: "\ stat \ a\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\Norm s0 \e-\b\ 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\Norm s0 \c1\ (x1, s1)" . have eval_c2: "G\Norm s1 \c2\ 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\Norm s0 \e-\v\ s1" . have s2:"s2 = abupd (raise_if (\ G,store s1\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\\(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\Norm s0 \e0-\b\ s1" . have eval_e1_e2: "G\s1 \(if the_Bool b then e1 else e2)-\v\ 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\Norm s0 \body G D sig-\v\ 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\Norm s0 \e-\v\ s1" . have eval_es: "G\s1 \es\\vs\ s2" .