# HG changeset patch
# User schirmer
# Date 1036152988 -3600
# Node ID ac335b2f4a39ba4cad2153f55b83ef48cd09ef70
# Parent  3d4ad560b2ff3bc896facf4f815c4badffa8f537
Inserted some extra paragraphs in large proofs to make tex run...

diff -r 3d4ad560b2ff -r ac335b2f4a39 src/HOL/Bali/AxCompl.thy
--- a/src/HOL/Bali/AxCompl.thy	Fri Nov 01 10:35:50 2002 +0100
+++ b/src/HOL/Bali/AxCompl.thy	Fri Nov 01 13:16:28 2002 +0100
@@ -1047,15 +1047,6 @@
   qed
 qed
 
-(* To term *)
-lemma term_cases: "
-  \<lbrakk>\<And> v. P \<langle>v\<rangle>\<^sub>v; \<And> e. P \<langle>e\<rangle>\<^sub>e;\<And> c. P \<langle>c\<rangle>\<^sub>s;\<And> l. P \<langle>l\<rangle>\<^sub>l\<rbrakk>
-  \<Longrightarrow> P t"
-  apply (cases t)
-  apply (case_tac a)
-  apply auto
-  done
-
 lemma MGFn_lemma:
   assumes mgf_methds: 
            "\<And> n. \<forall> C sig. G,(A::state triple set)\<turnstile>{=:n} \<langle>Methd C sig\<rangle>\<^sub>e\<succ> {G\<rightarrow>}"
@@ -1243,6 +1234,10 @@
       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
diff -r 3d4ad560b2ff -r ac335b2f4a39 src/HOL/Bali/AxSound.thy
--- a/src/HOL/Bali/AxSound.thy	Fri Nov 01 10:35:50 2002 +0100
+++ b/src/HOL/Bali/AxSound.thy	Fri Nov 01 13:16:28 2002 +0100
@@ -569,7 +569,11 @@
       ultimately show ?thesis using Q by simp
     qed
   qed
-next   
+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} }"
@@ -879,6 +883,10 @@
     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}
@@ -1216,6 +1224,10 @@
     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} }"
@@ -1799,6 +1811,10 @@
     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} }"
@@ -2202,6 +2218,10 @@
     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)
@@ -2473,6 +2493,10 @@
     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)
diff -r 3d4ad560b2ff -r ac335b2f4a39 src/HOL/Bali/DefiniteAssignmentCorrect.thy
--- a/src/HOL/Bali/DefiniteAssignmentCorrect.thy	Fri Nov 01 10:35:50 2002 +0100
+++ b/src/HOL/Bali/DefiniteAssignmentCorrect.thy	Fri Nov 01 13:16:28 2002 +0100
@@ -2829,6 +2829,10 @@
       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
@@ -3325,6 +3329,10 @@
       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 
@@ -3580,6 +3588,10 @@
       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
@@ -3881,6 +3893,10 @@
       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)))"
@@ -4271,6 +4287,10 @@
       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 3d4ad560b2ff -r ac335b2f4a39 src/HOL/Bali/Evaln.thy
--- a/src/HOL/Bali/Evaln.thy	Fri Nov 01 10:35:50 2002 +0100
+++ b/src/HOL/Bali/Evaln.thy	Fri Nov 01 13:16:28 2002 +0100
@@ -743,6 +743,10 @@
     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"
diff -r 3d4ad560b2ff -r ac335b2f4a39 src/HOL/Bali/Term.thy
--- a/src/HOL/Bali/Term.thy	Fri Nov 01 10:35:50 2002 +0100
+++ b/src/HOL/Bali/Term.thy	Fri Nov 01 13:16:28 2002 +0100
@@ -383,6 +383,14 @@
 lemma elist_var_inj_term [iff]: "\<langle>t::expr list\<rangle> \<noteq> \<langle>w::var\<rangle>"
   by (simp add: inj_term_simps)
 
+lemma term_cases: "
+  \<lbrakk>\<And> v. P \<langle>v\<rangle>\<^sub>v; \<And> e. P \<langle>e\<rangle>\<^sub>e;\<And> c. P \<langle>c\<rangle>\<^sub>s;\<And> l. P \<langle>l\<rangle>\<^sub>l\<rbrakk>
+  \<Longrightarrow> P t"
+  apply (cases t)
+  apply (case_tac a)
+  apply auto
+  done
+
 section {* Evaluation of unary operations *}
 consts eval_unop :: "unop \<Rightarrow> val \<Rightarrow> val"
 primrec
diff -r 3d4ad560b2ff -r ac335b2f4a39 src/HOL/Bali/TypeSafe.thy
--- a/src/HOL/Bali/TypeSafe.thy	Fri Nov 01 10:35:50 2002 +0100
+++ b/src/HOL/Bali/TypeSafe.thy	Fri Nov 01 13:16:28 2002 +0100
@@ -1938,6 +1938,10 @@
           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)" .
@@ -2228,6 +2232,10 @@
       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" .
@@ -2506,6 +2514,10 @@
           (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" .
@@ -2719,6 +2731,10 @@
            (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)" .
@@ -3342,6 +3358,10 @@
       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)" .
@@ -3707,6 +3727,10 @@
     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" .