--- 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)
--- 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 -
--- 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 ..