--- a/src/HOL/Bali/Trans.thy Wed Mar 12 22:57:50 2014 +0100
+++ b/src/HOL/Bali/Trans.thy Thu Mar 13 07:07:07 2014 +0100
@@ -23,12 +23,7 @@
| (FVar) accC statDeclC stat a fn where "v={accC,statDeclC,stat}(Lit a)..fn"
| (AVar) a i where "v=(Lit a).[Lit i]"
using ground LVar FVar AVar
- apply (cases v)
- apply (simp add: groundVar_def)
- apply (simp add: groundVar_def,blast)
- apply (simp add: groundVar_def,blast)
- apply (simp add: groundVar_def)
- done
+ by (cases v) (auto simp add: groundVar_def)
definition
groundExprs :: "expr list \<Rightarrow> bool"