src/HOL/Bali/WellType.thy
changeset 35416 d8d7d1b785af
parent 35067 af4c18c30593
child 35431 8758fe1fc9f8
     1.1 --- a/src/HOL/Bali/WellType.thy	Wed Feb 24 11:55:52 2010 +0100
     1.2 +++ b/src/HOL/Bali/WellType.thy	Mon Mar 01 13:40:23 2010 +0100
     1.3 @@ -53,11 +53,10 @@
     1.4    emhead = "ref_ty \<times> mhead"
     1.5  
     1.6  --{* Some mnemotic selectors for emhead *}
     1.7 -constdefs 
     1.8 -  "declrefT" :: "emhead \<Rightarrow> ref_ty"
     1.9 +definition "declrefT" :: "emhead \<Rightarrow> ref_ty" where
    1.10    "declrefT \<equiv> fst"
    1.11  
    1.12 -  "mhd"     :: "emhead \<Rightarrow> mhead"
    1.13 +definition "mhd"     :: "emhead \<Rightarrow> mhead" where
    1.14    "mhd \<equiv> snd"
    1.15  
    1.16  lemma declrefT_simp[simp]:"declrefT (r,m) = r"
    1.17 @@ -138,11 +137,10 @@
    1.18  done
    1.19  
    1.20  
    1.21 -constdefs
    1.22 -  empty_dt :: "dyn_ty"
    1.23 +definition empty_dt :: "dyn_ty" where
    1.24   "empty_dt \<equiv> \<lambda>a. None"
    1.25  
    1.26 -  invmode :: "('a::type)member_scheme \<Rightarrow> expr \<Rightarrow> inv_mode"
    1.27 +definition invmode :: "('a::type)member_scheme \<Rightarrow> expr \<Rightarrow> inv_mode" where
    1.28  "invmode m e \<equiv> if is_static m 
    1.29                    then Static 
    1.30                    else if e=Super then SuperM else IntVir"