src/HOL/Bali/Trans.thy
changeset 35416 d8d7d1b785af
parent 35069 09154b995ed8
child 37597 a02ea93e88c6
     1.1 --- a/src/HOL/Bali/Trans.thy	Wed Feb 24 11:55:52 2010 +0100
     1.2 +++ b/src/HOL/Bali/Trans.thy	Mon Mar 01 13:40:23 2010 +0100
     1.3 @@ -9,7 +9,7 @@
     1.4  
     1.5  theory Trans imports Evaln begin
     1.6  
     1.7 -constdefs groundVar:: "var \<Rightarrow> bool"
     1.8 +definition groundVar :: "var \<Rightarrow> bool" where
     1.9  "groundVar v \<equiv> (case v of
    1.10                     LVar ln \<Rightarrow> True
    1.11                   | {accC,statDeclC,stat}e..fn \<Rightarrow> \<exists> a. e=Lit a
    1.12 @@ -34,7 +34,7 @@
    1.13      done
    1.14  qed
    1.15  
    1.16 -constdefs groundExprs:: "expr list \<Rightarrow> bool"
    1.17 +definition groundExprs :: "expr list \<Rightarrow> bool" where
    1.18  "groundExprs es \<equiv> list_all (\<lambda> e. \<exists> v. e=Lit v) es"
    1.19    
    1.20  consts the_val:: "expr \<Rightarrow> val"