src/HOL/Bali/Term.thy
changeset 35416 d8d7d1b785af
parent 35315 fbdc860d87a3
child 35431 8758fe1fc9f8
     1.1 --- a/src/HOL/Bali/Term.thy	Wed Feb 24 11:55:52 2010 +0100
     1.2 +++ b/src/HOL/Bali/Term.thy	Mon Mar 01 13:40:23 2010 +0100
     1.3 @@ -261,9 +261,7 @@
     1.4    StatRef :: "ref_ty \<Rightarrow> expr"
     1.5    where "StatRef rt == Cast (RefT rt) (Lit Null)"
     1.6    
     1.7 -constdefs
     1.8 -
     1.9 -  is_stmt :: "term \<Rightarrow> bool"
    1.10 +definition is_stmt :: "term \<Rightarrow> bool" where
    1.11   "is_stmt t \<equiv> \<exists>c. t=In1r c"
    1.12  
    1.13  ML {* bind_thms ("is_stmt_rews", sum3_instantiate @{context} @{thm is_stmt_def}) *}
    1.14 @@ -467,7 +465,7 @@
    1.15  "eval_binop CondAnd v1 v2 = Bool ((the_Bool v1) \<and> (the_Bool v2))"
    1.16  "eval_binop CondOr  v1 v2 = Bool ((the_Bool v1) \<or> (the_Bool v2))"
    1.17  
    1.18 -constdefs need_second_arg :: "binop \<Rightarrow> val \<Rightarrow> bool"
    1.19 +definition need_second_arg :: "binop \<Rightarrow> val \<Rightarrow> bool" where
    1.20  "need_second_arg binop v1 \<equiv> \<not> ((binop=CondAnd \<and>  \<not> the_Bool v1) \<or>
    1.21                                 (binop=CondOr  \<and> the_Bool v1))"
    1.22  text {* @{term CondAnd} and @{term CondOr} only evalulate the second argument