src/HOL/Bali/TypeSafe.thy
changeset 18249 4398f0f12579
parent 17876 b9c92f384109
child 18447 da548623916a
     1.1 --- a/src/HOL/Bali/TypeSafe.thy	Fri Nov 25 18:58:34 2005 +0100
     1.2 +++ b/src/HOL/Bali/TypeSafe.thy	Fri Nov 25 18:58:35 2005 +0100
     1.3 @@ -939,11 +939,6 @@
     1.4  
     1.5  subsection "accessibility"
     1.6  
     1.7 -text {* 
     1.8 -\par
     1.9 -*} (* dummy text command to break paragraph for latex;
    1.10 -              large paragraphs exhaust memory of debian pdflatex *)
    1.11 -
    1.12  theorem dynamic_field_access_ok:
    1.13    assumes wf: "wf_prog G" and
    1.14      not_Null: "\<not> stat \<longrightarrow> a\<noteq>Null" and
    1.15 @@ -1922,10 +1917,6 @@
    1.16            a boolean value is part of @{term hyp_e}. See also Loop 
    1.17         *}
    1.18    next
    1.19 --- {* 
    1.20 -\par
    1.21 -*} (* dummy text command to break paragraph for latex;
    1.22 -              large paragraphs exhaust memory of debian pdflatex *)
    1.23      case (Loop b c e l s0 s1 s2 s3 L accC T A)
    1.24      have eval_e: "G\<turnstile>Norm s0 \<midarrow>e-\<succ>b\<rightarrow> s1" .
    1.25      have hyp_e: "PROP ?TypeSafe (Norm s0) s1 (In1l e) (In1 b)" .
    1.26 @@ -2216,10 +2207,6 @@
    1.27        qed
    1.28      qed
    1.29    next
    1.30 --- {* 
    1.31 -\par
    1.32 -*} (* dummy text command to break paragraph for latex;
    1.33 -              large paragraphs exhaust memory of debian pdflatex *)
    1.34      case (Fin c1 c2 s0 s1 s2 s3 x1 L accC T A)
    1.35      have eval_c1: "G\<turnstile>Norm s0 \<midarrow>c1\<rightarrow> (x1, s1)" .
    1.36      have eval_c2: "G\<turnstile>Norm s1 \<midarrow>c2\<rightarrow> s2" .
    1.37 @@ -2498,10 +2485,6 @@
    1.38            (error_free (Norm s0) = error_free s3) "
    1.39        by simp
    1.40    next
    1.41 --- {* 
    1.42 -\par
    1.43 -*} (* dummy text command to break paragraph for latex;
    1.44 -              large paragraphs exhaust memory of debian pdflatex *)
    1.45      case (Cast castT e s0 s1 s2 v L accC T A)
    1.46      have "G\<turnstile>Norm s0 \<midarrow>e-\<succ>v\<rightarrow> s1" .
    1.47      have s2:"s2 = abupd (raise_if (\<not> G,store s1\<turnstile>v fits castT) ClassCast) s1" .
    1.48 @@ -2715,10 +2698,6 @@
    1.49             (error_free (Norm s) = error_free (Norm s))"
    1.50        by simp
    1.51    next
    1.52 --- {* 
    1.53 -\par
    1.54 -*} (* dummy text command to break paragraph for latex;
    1.55 -              large paragraphs exhaust memory of debian pdflatex *)
    1.56      case (Acc upd s0 s1 w v L accC T A) 
    1.57      have hyp: "PROP ?TypeSafe (Norm s0) s1 (In2 v) (In2 (w,upd))" .
    1.58      have conf_s0: "Norm s0\<Colon>\<preceq>(G, L)" .
    1.59 @@ -2916,10 +2895,6 @@
    1.60        qed
    1.61      qed
    1.62    next
    1.63 --- {* 
    1.64 -\par
    1.65 -*} (* dummy text command to break paragraph for latex;
    1.66 -              large paragraphs exhaust memory of debian pdflatex *)
    1.67      case (Cond b e0 e1 e2 s0 s1 s2 v L accC T A)
    1.68      have eval_e0: "G\<turnstile>Norm s0 \<midarrow>e0-\<succ>b\<rightarrow> s1" .
    1.69      have eval_e1_e2: "G\<turnstile>s1 \<midarrow>(if the_Bool b then e1 else e2)-\<succ>v\<rightarrow> s2" .
    1.70 @@ -3357,10 +3332,6 @@
    1.71        qed
    1.72      qed
    1.73    next
    1.74 --- {* 
    1.75 -\par
    1.76 -*} (* dummy text command to break paragraph for latex;
    1.77 -              large paragraphs exhaust memory of debian pdflatex *)
    1.78      case (Methd D s0 s1 sig v L accC T A)
    1.79      have "G\<turnstile>Norm s0 \<midarrow>body G D sig-\<succ>v\<rightarrow> s1" .
    1.80      have hyp:"PROP ?TypeSafe (Norm s0) s1 (In1l (body G D sig)) (In1 v)" .
    1.81 @@ -3726,10 +3697,6 @@
    1.82      then show ?case
    1.83        by (auto elim!: wt_elim_cases)
    1.84    next
    1.85 --- {* 
    1.86 -\par
    1.87 -*} (* dummy text command to break paragraph for latex;
    1.88 -              large paragraphs exhaust memory of debian pdflatex *)
    1.89      case (Cons e es s0 s1 s2 v vs L accC T A)
    1.90      have eval_e: "G\<turnstile>Norm s0 \<midarrow>e-\<succ>v\<rightarrow> s1" .
    1.91      have eval_es: "G\<turnstile>s1 \<midarrow>es\<doteq>\<succ>vs\<rightarrow> s2" .