src/HOL/Bali/Trans.thy
changeset 56073 29e308b56d23
parent 47176 568fdc70e565
child 62042 6c6ccf573479
     1.1 --- a/src/HOL/Bali/Trans.thy	Wed Mar 12 22:57:50 2014 +0100
     1.2 +++ b/src/HOL/Bali/Trans.thy	Thu Mar 13 07:07:07 2014 +0100
     1.3 @@ -23,12 +23,7 @@
     1.4      | (FVar) accC statDeclC stat a fn where "v={accC,statDeclC,stat}(Lit a)..fn"
     1.5      | (AVar) a i where "v=(Lit a).[Lit i]"
     1.6    using ground LVar FVar AVar
     1.7 -  apply (cases v)
     1.8 -  apply (simp add: groundVar_def)
     1.9 -  apply (simp add: groundVar_def,blast)
    1.10 -  apply (simp add: groundVar_def,blast)
    1.11 -  apply (simp add: groundVar_def)
    1.12 -  done
    1.13 +  by (cases v) (auto simp add: groundVar_def)
    1.14  
    1.15  definition
    1.16    groundExprs :: "expr list \<Rightarrow> bool"