src/HOL/Bali/Basis.thy
changeset 35417 47ee18b6ae32
parent 35355 613e133966ea
parent 35416 d8d7d1b785af
child 35431 8758fe1fc9f8
     1.1 --- a/src/HOL/Bali/Basis.thy	Mon Mar 01 12:30:55 2010 +0100
     1.2 +++ b/src/HOL/Bali/Basis.thy	Mon Mar 01 13:42:31 2010 +0100
     1.3 @@ -237,8 +237,7 @@
     1.4  
     1.5  text{* Deemed too special for theory Map. *}
     1.6  
     1.7 -constdefs
     1.8 -  chg_map :: "('b => 'b) => 'a => ('a ~=> 'b) => ('a ~=> 'b)"
     1.9 +definition chg_map :: "('b => 'b) => 'a => ('a ~=> 'b) => ('a ~=> 'b)" where
    1.10   "chg_map f a m == case m a of None => m | Some b => m(a|->f b)"
    1.11  
    1.12  lemma chg_map_new[simp]: "m a = None   ==> chg_map f a m = m"
    1.13 @@ -253,8 +252,7 @@
    1.14  
    1.15  section "unique association lists"
    1.16  
    1.17 -constdefs
    1.18 -  unique   :: "('a \<times> 'b) list \<Rightarrow> bool"
    1.19 +definition unique :: "('a \<times> 'b) list \<Rightarrow> bool" where
    1.20   "unique \<equiv> distinct \<circ> map fst"
    1.21  
    1.22  lemma uniqueD [rule_format (no_asm)]: