# HG changeset patch
# User wenzelm
# Date 1135207721 -3600
# Node ID 2b102759160da870677dc2ad2aba795ad6f88257
# Parent  c0794cdbc6d1f3087b4426ce9359826b5bc5b651
mutual induct with *.inducts;

diff -r c0794cdbc6d1 -r 2b102759160d src/HOL/Bali/AxCompl.thy
--- a/src/HOL/Bali/AxCompl.thy	Thu Dec 22 00:28:39 2005 +0100
+++ b/src/HOL/Bali/AxCompl.thy	Thu Dec 22 00:28:41 2005 +0100
@@ -1062,7 +1062,7 @@
       "G,A\<turnstile>{=:n} \<langle>e\<rangle>\<^sub>e\<succ> {G\<rightarrow>}" and
       "G,A\<turnstile>{=:n} \<langle>c\<rangle>\<^sub>s\<succ> {G\<rightarrow>}" and  
       "G,A\<turnstile>{=:n} \<langle>es\<rangle>\<^sub>l\<succ> {G\<rightarrow>}"
-    proof (induct rule: var_expr_stmt.induct)
+    proof (induct rule: var_expr_stmt.inducts)
       case (LVar v)
       show "G,A\<turnstile>{=:n} \<langle>LVar v\<rangle>\<^sub>v\<succ> {G\<rightarrow>}"
 	apply (rule MGFn_NormalI)
diff -r c0794cdbc6d1 -r 2b102759160d src/HOL/Bali/DefiniteAssignment.thy
--- a/src/HOL/Bali/DefiniteAssignment.thy	Thu Dec 22 00:28:39 2005 +0100
+++ b/src/HOL/Bali/DefiniteAssignment.thy	Thu Dec 22 00:28:41 2005 +0100
@@ -337,7 +337,7 @@
   shows   "assigns_if b e = {}" (is "?Ass b e")
 proof -
   have "True" and "\<And> b. ?Const b e \<Longrightarrow> ?Ass b e" and "True" and "True"
-  proof (induct _ and e and _ and _ rule: var_expr_stmt.induct) 
+  proof (induct _ and e and _ and _ rule: var_expr_stmt.inducts)
     case Lit
     thus ?case by simp
   next
@@ -382,10 +382,10 @@
 
 lemma assigns_if_const_not_b_simp:
   assumes boolConst: "constVal e = Some (Bool b)"        (is "?Const b e")  
-    shows "assigns_if (\<not>b) e = UNIV"                    (is "?Ass b e")
+  shows "assigns_if (\<not>b) e = UNIV"                  (is "?Ass b e")
 proof -
   have True and "\<And> b. ?Const b e \<Longrightarrow> ?Ass b e" and True and True
-  proof (induct _ and e and _ and _ rule: var_expr_stmt.induct) 
+  proof (induct _ and e and _ and _ rule: var_expr_stmt.inducts) 
     case Lit
     thus ?case by simp
   next
@@ -963,7 +963,7 @@
    shows "assignsE e \<subseteq> assigns_if True e \<inter> assigns_if False e" (is "?Incl e")
 proof -
   have True and "?Boolean e \<Longrightarrow> ?Incl e" and True and True
-  proof (induct _ and e and _ and _ rule: var_expr_stmt.induct)
+  proof (induct _ and e and _ and _ rule: var_expr_stmt.inducts)
     case (Cast T e)
     have "E\<turnstile>e\<Colon>- (PrimT Boolean)"
     proof -
diff -r c0794cdbc6d1 -r 2b102759160d src/HOL/Bali/DefiniteAssignmentCorrect.thy
--- a/src/HOL/Bali/DefiniteAssignmentCorrect.thy	Thu Dec 22 00:28:39 2005 +0100
+++ b/src/HOL/Bali/DefiniteAssignmentCorrect.thy	Thu Dec 22 00:28:41 2005 +0100
@@ -105,7 +105,7 @@
     have True and True and 
        "\<And> jmps' jmps. \<lbrakk>jumpNestingOkS jmps' c; jmps' \<subseteq> jmps\<rbrakk> \<Longrightarrow> jumpNestingOkS jmps c" 
        and True
-  proof (induct rule: var_expr_stmt.induct)
+  proof (induct rule: var_expr_stmt.inducts)
     case (Lab j c jmps' jmps)
     have jmpOk: "jumpNestingOkS jmps' (j\<bullet> c)" .
     have jmps: "jmps' \<subseteq> jmps" .
@@ -2017,7 +2017,7 @@
         "\<And> c v s0 s. \<lbrakk> constVal e = Some c; G\<turnstile>Norm s0 \<midarrow>e-\<succ>v\<rightarrow> s\<rbrakk> 
                       \<Longrightarrow> v = c \<and> normal s"
         and True and True
-  proof (induct  rule: var_expr_stmt.induct)
+  proof (induct  rule: var_expr_stmt.inducts)
     case NewC hence False by simp thus ?case ..
   next
     case NewA hence False by simp thus ?case ..
@@ -2165,7 +2165,7 @@
        "\<And> c. \<lbrakk>constVal e = Some c;Env\<turnstile>e\<Colon>-PrimT Boolean\<rbrakk> 
                 \<Longrightarrow> typeof empty_dt c = Some (PrimT Boolean)"
        and True and True 
-  proof (induct rule: var_expr_stmt.induct)
+  proof (induct rule: var_expr_stmt.inducts)
     case NewC hence False by simp thus ?case ..
   next
     case NewA hence False by simp thus ?case ..