src/HOL/Bali/Table.thy
changeset 14025 d9b155757dc8
parent 13688 a0b16d42d489
child 14134 0fdf5708c7a8
     1.1 --- a/src/HOL/Bali/Table.thy	Tue May 13 08:59:21 2003 +0200
     1.2 +++ b/src/HOL/Bali/Table.thy	Wed May 14 10:22:09 2003 +0200
     1.3 @@ -49,9 +49,9 @@
     1.4    (type)"('a, 'b) table" <= (type)"'a \<leadsto> 'b"
     1.5  
     1.6  (* ### To map *)
     1.7 -lemma override_find_left[simp]:
     1.8 +lemma map_add_find_left[simp]:
     1.9  "n k = None \<Longrightarrow> (m ++ n) k = m k"
    1.10 -by (simp add: override_def)
    1.11 +by (simp add: map_add_def)
    1.12  
    1.13  section {* Conditional Override *}
    1.14  constdefs
    1.15 @@ -278,8 +278,8 @@
    1.16  
    1.17  lemma table_append_Some_iff: "table_of (xs@ys) k = Some z = 
    1.18   (table_of xs k = Some z \<or> (table_of xs k = None \<and> table_of ys k = Some z))"
    1.19 -apply (simp only: map_of_override [THEN sym])
    1.20 -apply (rule override_Some_iff)
    1.21 +apply (simp)
    1.22 +apply (rule map_add_Some_iff)
    1.23  done
    1.24  
    1.25  lemma table_of_filter_unique_SomeD [rule_format (no_asm)]: