src/HOL/Bali/TypeSafe.thy
changeset 13690 ac335b2f4a39
parent 13688 a0b16d42d489
child 14030 cd928c0ac225
     1.1 --- a/src/HOL/Bali/TypeSafe.thy	Fri Nov 01 10:35:50 2002 +0100
     1.2 +++ b/src/HOL/Bali/TypeSafe.thy	Fri Nov 01 13:16:28 2002 +0100
     1.3 @@ -1938,6 +1938,10 @@
     1.4            a boolean value is part of @{term hyp_e}. See also Loop 
     1.5         *}
     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 (Loop b c e l s0 s1 s2 s3 L accC T A)
    1.12      have eval_e: "G\<turnstile>Norm s0 \<midarrow>e-\<succ>b\<rightarrow> s1" .
    1.13      have hyp_e: "PROP ?TypeSafe (Norm s0) s1 (In1l e) (In1 b)" .
    1.14 @@ -2228,6 +2232,10 @@
    1.15        qed
    1.16      qed
    1.17    next
    1.18 +-- {* 
    1.19 +\par
    1.20 +*} (* dummy text command to break paragraph for latex;
    1.21 +              large paragraphs exhaust memory of debian pdflatex *)
    1.22      case (Fin c1 c2 s0 s1 s2 s3 x1 L accC T A)
    1.23      have eval_c1: "G\<turnstile>Norm s0 \<midarrow>c1\<rightarrow> (x1, s1)" .
    1.24      have eval_c2: "G\<turnstile>Norm s1 \<midarrow>c2\<rightarrow> s2" .
    1.25 @@ -2506,6 +2514,10 @@
    1.26            (error_free (Norm s0) = error_free s3) "
    1.27        by simp
    1.28    next
    1.29 +-- {* 
    1.30 +\par
    1.31 +*} (* dummy text command to break paragraph for latex;
    1.32 +              large paragraphs exhaust memory of debian pdflatex *)
    1.33      case (Cast castT e s0 s1 s2 v L accC T A)
    1.34      have "G\<turnstile>Norm s0 \<midarrow>e-\<succ>v\<rightarrow> s1" .
    1.35      have s2:"s2 = abupd (raise_if (\<not> G,store s1\<turnstile>v fits castT) ClassCast) s1" .
    1.36 @@ -2719,6 +2731,10 @@
    1.37             (error_free (Norm s) = error_free (Norm s))"
    1.38        by simp
    1.39    next
    1.40 +-- {* 
    1.41 +\par
    1.42 +*} (* dummy text command to break paragraph for latex;
    1.43 +              large paragraphs exhaust memory of debian pdflatex *)
    1.44      case (Acc upd s0 s1 w v L accC T A) 
    1.45      have hyp: "PROP ?TypeSafe (Norm s0) s1 (In2 v) (In2 (w,upd))" .
    1.46      have conf_s0: "Norm s0\<Colon>\<preceq>(G, L)" .
    1.47 @@ -3342,6 +3358,10 @@
    1.48        qed
    1.49      qed
    1.50    next
    1.51 +-- {* 
    1.52 +\par
    1.53 +*} (* dummy text command to break paragraph for latex;
    1.54 +              large paragraphs exhaust memory of debian pdflatex *)
    1.55      case (Methd D s0 s1 sig v L accC T A)
    1.56      have "G\<turnstile>Norm s0 \<midarrow>body G D sig-\<succ>v\<rightarrow> s1" .
    1.57      have hyp:"PROP ?TypeSafe (Norm s0) s1 (In1l (body G D sig)) (In1 v)" .
    1.58 @@ -3707,6 +3727,10 @@
    1.59      then show ?case
    1.60        by (auto elim!: wt_elim_cases)
    1.61    next
    1.62 +-- {* 
    1.63 +\par
    1.64 +*} (* dummy text command to break paragraph for latex;
    1.65 +              large paragraphs exhaust memory of debian pdflatex *)
    1.66      case (Cons e es s0 s1 s2 v vs L accC T A)
    1.67      have eval_e: "G\<turnstile>Norm s0 \<midarrow>e-\<succ>v\<rightarrow> s1" .
    1.68      have eval_es: "G\<turnstile>s1 \<midarrow>es\<doteq>\<succ>vs\<rightarrow> s2" .