diff -r f87d1105e181 -r ee939247b2fb src/HOL/Bali/Trans.thy
--- a/src/HOL/Bali/Trans.thy	Mon Jul 26 13:50:52 2010 +0200
+++ b/src/HOL/Bali/Trans.thy	Mon Jul 26 17:41:26 2010 +0200
@@ -9,12 +9,13 @@
 
 theory Trans imports Evaln begin
 
-definition groundVar :: "var \<Rightarrow> bool" where
-"groundVar v \<longleftrightarrow> (case v of
-                   LVar ln \<Rightarrow> True
-                 | {accC,statDeclC,stat}e..fn \<Rightarrow> \<exists> a. e=Lit a
-                 | e1.[e2] \<Rightarrow> \<exists> a i. e1= Lit a \<and> e2 = Lit i
-                 | InsInitV c v \<Rightarrow> False)"
+definition
+  groundVar :: "var \<Rightarrow> bool" where
+  "groundVar v \<longleftrightarrow> (case v of
+                     LVar ln \<Rightarrow> True
+                   | {accC,statDeclC,stat}e..fn \<Rightarrow> \<exists> a. e=Lit a
+                   | e1.[e2] \<Rightarrow> \<exists> a i. e1= Lit a \<and> e2 = Lit i
+                   | InsInitV c v \<Rightarrow> False)"
 
 lemma groundVar_cases [consumes 1, case_names LVar FVar AVar]:
   assumes ground: "groundVar v" and
@@ -34,14 +35,15 @@
     done
 qed
 
-definition groundExprs :: "expr list \<Rightarrow> bool" where
-  "groundExprs es \<longleftrightarrow> (\<forall>e \<in> set es. \<exists>v. e = Lit v)"
+definition
+  groundExprs :: "expr list \<Rightarrow> bool"
+  where "groundExprs es \<longleftrightarrow> (\<forall>e \<in> set es. \<exists>v. e = Lit v)"
   
-primrec the_val:: "expr \<Rightarrow> val" where
-  "the_val (Lit v) = v"
+primrec the_val:: "expr \<Rightarrow> val"
+  where "the_val (Lit v) = v"
 
 primrec the_var:: "prog \<Rightarrow> state \<Rightarrow> var \<Rightarrow> (vvar \<times> state)" where
-  "the_var G s (LVar ln)                    =(lvar ln (store s),s)"
+  "the_var G s (LVar ln) = (lvar ln (store s),s)"
 | the_var_FVar_def: "the_var G s ({accC,statDeclC,stat}a..fn) =fvar statDeclC stat fn (the_val a) s"
 | the_var_AVar_def: "the_var G s(a.[i])                       =avar G (the_val i) (the_val a) s"