removed obsolete dummy paragraphs;
authorwenzelm
Fri Nov 25 18:58:35 2005 +0100 (2005-11-25)
changeset 182494398f0f12579
parent 18248 929659a46ecf
child 18250 dfe5d09514eb
removed obsolete dummy paragraphs;
src/HOL/Bali/AxCompl.thy
src/HOL/Bali/AxSound.thy
src/HOL/Bali/DefiniteAssignmentCorrect.thy
src/HOL/Bali/Eval.thy
src/HOL/Bali/Evaln.thy
src/HOL/Bali/TypeSafe.thy
     1.1 --- a/src/HOL/Bali/AxCompl.thy	Fri Nov 25 18:58:34 2005 +0100
     1.2 +++ b/src/HOL/Bali/AxCompl.thy	Fri Nov 25 18:58:35 2005 +0100
     1.3 @@ -1233,10 +1233,6 @@
     1.4        show "G,A\<turnstile>{=:n} \<langle>Methd D mn\<rangle>\<^sub>e\<succ> {G\<rightarrow>}"
     1.5  	by simp
     1.6      next
     1.7 --- {* 
     1.8 -\par
     1.9 -*} (* dummy text command to break paragraph for latex;
    1.10 -              large paragraphs exhaust memory of debian pdflatex *)
    1.11        case (Body D c)
    1.12        have mgf_c: "G,A\<turnstile>{=:n} \<langle>c\<rangle>\<^sub>s\<succ> {G\<rightarrow>}" .
    1.13        from wf MGFn_Init [OF hyp] mgf_c
     2.1 --- a/src/HOL/Bali/AxSound.thy	Fri Nov 25 18:58:34 2005 +0100
     2.2 +++ b/src/HOL/Bali/AxSound.thy	Fri Nov 25 18:58:35 2005 +0100
     2.3 @@ -569,10 +569,6 @@
     2.4      qed
     2.5    qed
     2.6  next
     2.7 --- {* 
     2.8 -\par
     2.9 -*} (* dummy text command to break paragraph for latex;
    2.10 -              large paragraphs exhaust memory of debian pdflatex *)   
    2.11    case (AVar A P Q R e1 e2)
    2.12    have valid_e1: "G,A|\<Turnstile>\<Colon>{ {Normal P} e1-\<succ> {Q} }" .
    2.13    have valid_e2: "\<And> a. G,A|\<Turnstile>\<Colon>{ {Q\<leftarrow>In1 a} e2-\<succ> {\<lambda>Val:i:. avar G i a ..; R} }"
    2.14 @@ -882,10 +878,6 @@
    2.15      qed
    2.16    qed
    2.17  next
    2.18 --- {* 
    2.19 -\par
    2.20 -*} (* dummy text command to break paragraph for latex;
    2.21 -              large paragraphs exhaust memory of debian pdflatex *)
    2.22    case (BinOp A P Q R binop e1 e2)
    2.23    assume valid_e1: "G,A|\<Turnstile>\<Colon>{ {Normal P} e1-\<succ> {Q} }" 
    2.24    have valid_e2: "\<And> v1.  G,A|\<Turnstile>\<Colon>{ {Q\<leftarrow>In1 v1}
    2.25 @@ -1223,10 +1215,6 @@
    2.26      qed
    2.27    qed
    2.28  next
    2.29 --- {* 
    2.30 -\par
    2.31 -*} (* dummy text command to break paragraph for latex;
    2.32 -              large paragraphs exhaust memory of debian pdflatex *)
    2.33    case (Call A P Q R S accC' args e mn mode pTs' statT)
    2.34    have valid_e: "G,A|\<Turnstile>\<Colon>{ {Normal P} e-\<succ> {Q} }" .
    2.35    have valid_args: "\<And> a. G,A|\<Turnstile>\<Colon>{ {Q\<leftarrow>In1 a} args\<doteq>\<succ> {R a} }"
    2.36 @@ -1611,10 +1599,6 @@
    2.37      qed
    2.38    qed
    2.39  next
    2.40 --- {* 
    2.41 -\par
    2.42 -*} (* dummy text command to break paragraph for latex;
    2.43 -              large paragraphs exhaust memory of debian pdflatex *)
    2.44    case (Methd A P Q ms)
    2.45    have valid_body: "G,A \<union> {{P} Methd-\<succ> {Q} | ms}|\<Turnstile>\<Colon>{{P} body G-\<succ> {Q} | ms}".
    2.46    show "G,A|\<Turnstile>\<Colon>{{P} Methd-\<succ> {Q} | ms}"
    2.47 @@ -1825,10 +1809,6 @@
    2.48      qed
    2.49    qed
    2.50  next
    2.51 --- {* 
    2.52 -\par
    2.53 -*} (* dummy text command to break paragraph for latex;
    2.54 -              large paragraphs exhaust memory of debian pdflatex *)
    2.55    case (Lab A P Q c l)
    2.56    have valid_c: "G,A|\<Turnstile>\<Colon>{ {Normal P} .c. {abupd (absorb l) .; Q} }".
    2.57    show "G,A|\<Turnstile>\<Colon>{ {Normal P} .l\<bullet> c. {Q} }"
    2.58 @@ -2232,10 +2212,6 @@
    2.59      qed
    2.60    qed
    2.61  next
    2.62 --- {* 
    2.63 -\par
    2.64 -*} (* dummy text command to break paragraph for latex;
    2.65 -              large paragraphs exhaust memory of debian pdflatex *)
    2.66    case (Jmp A P j)
    2.67    show "G,A|\<Turnstile>\<Colon>{ {Normal (abupd (\<lambda>a. Some (Jump j)) .; P\<leftarrow>\<diamondsuit>)} .Jmp j. {P} }"
    2.68    proof (rule valid_stmt_NormalI)
    2.69 @@ -2507,10 +2483,6 @@
    2.70      qed
    2.71    qed
    2.72  next
    2.73 --- {* 
    2.74 -\par
    2.75 -*} (* dummy text command to break paragraph for latex;
    2.76 -              large paragraphs exhaust memory of debian pdflatex *)
    2.77    case (Done A C P)
    2.78    show "G,A|\<Turnstile>\<Colon>{ {Normal (P\<leftarrow>\<diamondsuit> \<and>. initd C)} .Init C. {P} }" 
    2.79    proof (rule valid_stmt_NormalI)
     3.1 --- a/src/HOL/Bali/DefiniteAssignmentCorrect.thy	Fri Nov 25 18:58:34 2005 +0100
     3.2 +++ b/src/HOL/Bali/DefiniteAssignmentCorrect.thy	Fri Nov 25 18:58:35 2005 +0100
     3.3 @@ -2829,10 +2829,6 @@
     3.4        ultimately show ?thesis by (intro conjI)
     3.5      qed
     3.6    next
     3.7 --- {* 
     3.8 -\par
     3.9 -*} (* dummy text command to break paragraph for latex;
    3.10 -              large paragraphs exhaust memory of debian pdflatex *)
    3.11      case (If b c1 c2 e s0 s1 s2 Env T A)
    3.12      have G: "prg Env = G" .
    3.13      with If.hyps have eval_e: "prg Env \<turnstile>Norm s0 \<midarrow>e-\<succ>b\<rightarrow> s1" by simp
    3.14 @@ -2937,10 +2933,6 @@
    3.15        ultimately show ?thesis by simp
    3.16      qed
    3.17    next
    3.18 --- {* 
    3.19 -\par
    3.20 -*} (* dummy text command to break paragraph for latex;
    3.21 -              large paragraphs exhaust memory of debian pdflatex *)
    3.22      case (Loop b c e l s0 s1 s2 s3 Env T A)
    3.23      have G: "prg Env = G" .
    3.24      with Loop.hyps have eval_e: "prg Env\<turnstile>Norm s0 \<midarrow>e-\<succ>b\<rightarrow> s1" 
    3.25 @@ -3324,10 +3316,6 @@
    3.26        qed
    3.27      qed
    3.28    next
    3.29 --- {* 
    3.30 -\par
    3.31 -*} (* dummy text command to break paragraph for latex;
    3.32 -              large paragraphs exhaust memory of debian pdflatex *)
    3.33      case (Fin c1 c2 s0 s1 s2 s3 x1 Env T A)
    3.34      have G: "prg Env = G" .
    3.35      from Fin.prems obtain C1 C2 where 
    3.36 @@ -3583,10 +3571,6 @@
    3.37        by simp_all      
    3.38      ultimately show ?case by (intro conjI)
    3.39    next
    3.40 --- {* 
    3.41 -\par
    3.42 -*} (* dummy text command to break paragraph for latex;
    3.43 -              large paragraphs exhaust memory of debian pdflatex *)
    3.44      case (NewA elT a e i s0 s1 s2 s3 Env T A) 
    3.45      have G: "prg Env = G" .
    3.46      from NewA.prems obtain
    3.47 @@ -3888,10 +3872,6 @@
    3.48        by simp_all
    3.49      ultimately show ?case by (intro conjI) 
    3.50    next
    3.51 --- {* 
    3.52 -\par
    3.53 -*} (* dummy text command to break paragraph for latex;
    3.54 -              large paragraphs exhaust memory of debian pdflatex *)
    3.55      case (Super s Env T A)
    3.56      from Super.prems
    3.57      have "nrm A = dom (locals (store ((Norm s)::state)))"
    3.58 @@ -4042,10 +4022,6 @@
    3.59        by simp_all
    3.60      ultimately show ?case by (intro conjI)
    3.61    next
    3.62 --- {* 
    3.63 -\par
    3.64 -*} (* dummy text command to break paragraph for latex;
    3.65 -              large paragraphs exhaust memory of debian pdflatex *)
    3.66      case (Cond b e0 e1 e2 s0 s1 s2 v Env T A)
    3.67      have G: "prg Env = G" .
    3.68      have "?NormalAssigned s2 A"
    3.69 @@ -4282,10 +4258,6 @@
    3.70        by simp_all
    3.71      ultimately show ?case by (intro conjI)
    3.72    next
    3.73 --- {* 
    3.74 -\par
    3.75 -*} (* dummy text command to break paragraph for latex;
    3.76 -              large paragraphs exhaust memory of debian pdflatex *)
    3.77      case (LVar s vn Env T A)
    3.78      from LVar.prems
    3.79      have "nrm A = dom (locals (store ((Norm s)::state)))"
     4.1 --- a/src/HOL/Bali/Eval.thy	Fri Nov 25 18:58:34 2005 +0100
     4.2 +++ b/src/HOL/Bali/Eval.thy	Fri Nov 25 18:58:35 2005 +0100
     4.3 @@ -545,12 +545,6 @@
     4.4  	  G\<turnstile>(Some (Xcpt (Std xn)),s0) \<midarrow>sxalloc\<rightarrow> (Some (Xcpt (Loc a)),s1)"
     4.5  
     4.6  
     4.7 -text {* 
     4.8 -\par
     4.9 -*} (* dummy text command to break paragraph for latex;
    4.10 -              large paragraphs exhaust memory of debian pdflatex *)
    4.11 -
    4.12 -
    4.13  inductive "eval G" intros
    4.14  
    4.15  --{* propagation of abrupt completion *}
    4.16 @@ -793,11 +787,6 @@
    4.17  *}
    4.18  
    4.19  
    4.20 -text {* 
    4.21 -\par
    4.22 -*} (* dummy text command to break paragraph for latex;
    4.23 -              large paragraphs exhaust memory of debian pdflatex *)
    4.24 -
    4.25  lemmas eval_induct = eval_induct_ [split_format and and and and and and and and
    4.26     and and and and and and s1 (* Acc *) and and s2 (* Comp *) and and and and 
    4.27     and and 
     5.1 --- a/src/HOL/Bali/Evaln.thy	Fri Nov 25 18:58:34 2005 +0100
     5.2 +++ b/src/HOL/Bali/Evaln.thy	Fri Nov 25 18:58:35 2005 +0100
     5.3 @@ -742,10 +742,6 @@
     5.4      by (rule evaln.Super)
     5.5    then show ?case ..
     5.6  next
     5.7 --- {* 
     5.8 -\par
     5.9 -*} (* dummy text command to break paragraph for latex;
    5.10 -              large paragraphs exhaust memory of debian pdflatex *)
    5.11    case (Acc f s0 s1 v va)
    5.12    then obtain n where
    5.13      "G\<turnstile>Norm s0 \<midarrow>va=\<succ>(v, f)\<midarrow>n\<rightarrow> s1"
     6.1 --- a/src/HOL/Bali/TypeSafe.thy	Fri Nov 25 18:58:34 2005 +0100
     6.2 +++ b/src/HOL/Bali/TypeSafe.thy	Fri Nov 25 18:58:35 2005 +0100
     6.3 @@ -939,11 +939,6 @@
     6.4  
     6.5  subsection "accessibility"
     6.6  
     6.7 -text {* 
     6.8 -\par
     6.9 -*} (* dummy text command to break paragraph for latex;
    6.10 -              large paragraphs exhaust memory of debian pdflatex *)
    6.11 -
    6.12  theorem dynamic_field_access_ok:
    6.13    assumes wf: "wf_prog G" and
    6.14      not_Null: "\<not> stat \<longrightarrow> a\<noteq>Null" and
    6.15 @@ -1922,10 +1917,6 @@
    6.16            a boolean value is part of @{term hyp_e}. See also Loop 
    6.17         *}
    6.18    next
    6.19 --- {* 
    6.20 -\par
    6.21 -*} (* dummy text command to break paragraph for latex;
    6.22 -              large paragraphs exhaust memory of debian pdflatex *)
    6.23      case (Loop b c e l s0 s1 s2 s3 L accC T A)
    6.24      have eval_e: "G\<turnstile>Norm s0 \<midarrow>e-\<succ>b\<rightarrow> s1" .
    6.25      have hyp_e: "PROP ?TypeSafe (Norm s0) s1 (In1l e) (In1 b)" .
    6.26 @@ -2216,10 +2207,6 @@
    6.27        qed
    6.28      qed
    6.29    next
    6.30 --- {* 
    6.31 -\par
    6.32 -*} (* dummy text command to break paragraph for latex;
    6.33 -              large paragraphs exhaust memory of debian pdflatex *)
    6.34      case (Fin c1 c2 s0 s1 s2 s3 x1 L accC T A)
    6.35      have eval_c1: "G\<turnstile>Norm s0 \<midarrow>c1\<rightarrow> (x1, s1)" .
    6.36      have eval_c2: "G\<turnstile>Norm s1 \<midarrow>c2\<rightarrow> s2" .
    6.37 @@ -2498,10 +2485,6 @@
    6.38            (error_free (Norm s0) = error_free s3) "
    6.39        by simp
    6.40    next
    6.41 --- {* 
    6.42 -\par
    6.43 -*} (* dummy text command to break paragraph for latex;
    6.44 -              large paragraphs exhaust memory of debian pdflatex *)
    6.45      case (Cast castT e s0 s1 s2 v L accC T A)
    6.46      have "G\<turnstile>Norm s0 \<midarrow>e-\<succ>v\<rightarrow> s1" .
    6.47      have s2:"s2 = abupd (raise_if (\<not> G,store s1\<turnstile>v fits castT) ClassCast) s1" .
    6.48 @@ -2715,10 +2698,6 @@
    6.49             (error_free (Norm s) = error_free (Norm s))"
    6.50        by simp
    6.51    next
    6.52 --- {* 
    6.53 -\par
    6.54 -*} (* dummy text command to break paragraph for latex;
    6.55 -              large paragraphs exhaust memory of debian pdflatex *)
    6.56      case (Acc upd s0 s1 w v L accC T A) 
    6.57      have hyp: "PROP ?TypeSafe (Norm s0) s1 (In2 v) (In2 (w,upd))" .
    6.58      have conf_s0: "Norm s0\<Colon>\<preceq>(G, L)" .
    6.59 @@ -2916,10 +2895,6 @@
    6.60        qed
    6.61      qed
    6.62    next
    6.63 --- {* 
    6.64 -\par
    6.65 -*} (* dummy text command to break paragraph for latex;
    6.66 -              large paragraphs exhaust memory of debian pdflatex *)
    6.67      case (Cond b e0 e1 e2 s0 s1 s2 v L accC T A)
    6.68      have eval_e0: "G\<turnstile>Norm s0 \<midarrow>e0-\<succ>b\<rightarrow> s1" .
    6.69      have eval_e1_e2: "G\<turnstile>s1 \<midarrow>(if the_Bool b then e1 else e2)-\<succ>v\<rightarrow> s2" .
    6.70 @@ -3357,10 +3332,6 @@
    6.71        qed
    6.72      qed
    6.73    next
    6.74 --- {* 
    6.75 -\par
    6.76 -*} (* dummy text command to break paragraph for latex;
    6.77 -              large paragraphs exhaust memory of debian pdflatex *)
    6.78      case (Methd D s0 s1 sig v L accC T A)
    6.79      have "G\<turnstile>Norm s0 \<midarrow>body G D sig-\<succ>v\<rightarrow> s1" .
    6.80      have hyp:"PROP ?TypeSafe (Norm s0) s1 (In1l (body G D sig)) (In1 v)" .
    6.81 @@ -3726,10 +3697,6 @@
    6.82      then show ?case
    6.83        by (auto elim!: wt_elim_cases)
    6.84    next
    6.85 --- {* 
    6.86 -\par
    6.87 -*} (* dummy text command to break paragraph for latex;
    6.88 -              large paragraphs exhaust memory of debian pdflatex *)
    6.89      case (Cons e es s0 s1 s2 v vs L accC T A)
    6.90      have eval_e: "G\<turnstile>Norm s0 \<midarrow>e-\<succ>v\<rightarrow> s1" .
    6.91      have eval_es: "G\<turnstile>s1 \<midarrow>es\<doteq>\<succ>vs\<rightarrow> s2" .