--- a/src/HOL/Bali/DefiniteAssignmentCorrect.thy Tue Sep 09 20:51:36 2014 +0200
+++ b/src/HOL/Bali/DefiniteAssignmentCorrect.thy Tue Sep 09 20:51:36 2014 +0200
@@ -102,8 +102,7 @@
proof -
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.inducts)
+ proof (induct rule: var.induct expr.induct stmt.induct)
case (Lab j c jmps' jmps)
note jmpOk = `jumpNestingOkS jmps' (j\<bullet> c)`
note jmps = `jmps' \<subseteq> jmps`
@@ -2008,8 +2007,8 @@
have True and
"\<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.inducts)
+ and True
+ proof (induct rule: var.induct expr.induct stmt.induct)
case NewC hence False by simp thus ?case ..
next
case NewA hence False by simp thus ?case ..
@@ -2156,8 +2155,8 @@
have True and
"\<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.inducts)
+ and True
+ proof (induct rule: var.induct expr.induct stmt.induct)
case NewC hence False by simp thus ?case ..
next
case NewA hence False by simp thus ?case ..