src/HOL/Bali/Trans.thy

 PRELIMINARY!!!!!!!!
 *)
 
 theory Trans imports Evaln begin
 
-constdefs groundVar:: "var \<Rightarrow> bool"
+definition groundVar :: "var \<Rightarrow> bool" where
 "groundVar v \<equiv> (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)"

     apply (simp add: groundVar_def,blast)
     apply (simp add: groundVar_def)
     done
 qed
 
-constdefs groundExprs:: "expr list \<Rightarrow> bool"
+definition groundExprs :: "expr list \<Rightarrow> bool" where
 "groundExprs es \<equiv> list_all (\<lambda> e. \<exists> v. e=Lit v) es"
   
 consts the_val:: "expr \<Rightarrow> val"
 primrec
 "the_val (Lit v) = v"