src/HOL/Bali/Table.thy
changeset 35416 d8d7d1b785af
parent 34939 44294cfecb1d
child 35417 47ee18b6ae32
     1.1 --- a/src/HOL/Bali/Table.thy	Wed Feb 24 11:55:52 2010 +0100
     1.2 +++ b/src/HOL/Bali/Table.thy	Mon Mar 01 13:40:23 2010 +0100
     1.3 @@ -53,9 +53,7 @@
     1.4  by (simp add: map_add_def)
     1.5  
     1.6  section {* Conditional Override *}
     1.7 -constdefs
     1.8 -cond_override:: 
     1.9 -  "('b \<Rightarrow>'b \<Rightarrow> bool) \<Rightarrow> ('a, 'b)table \<Rightarrow> ('a, 'b)table \<Rightarrow> ('a, 'b) table"
    1.10 +definition cond_override :: "('b \<Rightarrow>'b \<Rightarrow> bool) \<Rightarrow> ('a, 'b)table \<Rightarrow> ('a, 'b)table \<Rightarrow> ('a, 'b) table" where
    1.11  
    1.12  --{* when merging tables old and new, only override an entry of table old when  
    1.13     the condition cond holds *}
    1.14 @@ -100,8 +98,7 @@
    1.15  
    1.16  section {* Filter on Tables *}
    1.17  
    1.18 -constdefs
    1.19 -filter_tab:: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('a, 'b) table \<Rightarrow> ('a, 'b) table"
    1.20 +definition filter_tab :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('a, 'b) table \<Rightarrow> ('a, 'b) table" where
    1.21  "filter_tab c t \<equiv> \<lambda> k. (case t k of 
    1.22                             None   \<Rightarrow> None
    1.23                           | Some x \<Rightarrow> if c k x then Some x else None)"