changeset 58251 | b13e5c3497f5 |
parent 56199 | 8e8d28ed7529 |
child 58887 | 38db8ddc0f57 |
--- a/src/HOL/Bali/Evaln.thy Tue Sep 09 20:51:36 2014 +0200 +++ b/src/HOL/Bali/Evaln.thy Tue Sep 09 20:51:36 2014 +0200 @@ -245,7 +245,7 @@ | In2 e \<Rightarrow> (\<exists>v. w = In2 v) | In3 e \<Rightarrow> (\<exists>v. w = In3 v)" apply (erule evaln_cases , auto) apply (induct_tac "t") -apply (induct_tac "a") +apply (rename_tac a, induct_tac "a") apply auto done