src/HOL/Bali/Table.thy
changeset 14025 d9b155757dc8
parent 13688 a0b16d42d489
child 14134 0fdf5708c7a8
--- a/src/HOL/Bali/Table.thy	Tue May 13 08:59:21 2003 +0200
+++ b/src/HOL/Bali/Table.thy	Wed May 14 10:22:09 2003 +0200
@@ -49,9 +49,9 @@
   (type)"('a, 'b) table" <= (type)"'a \<leadsto> 'b"
 
 (* ### To map *)
-lemma override_find_left[simp]:
+lemma map_add_find_left[simp]:
 "n k = None \<Longrightarrow> (m ++ n) k = m k"
-by (simp add: override_def)
+by (simp add: map_add_def)
 
 section {* Conditional Override *}
 constdefs
@@ -278,8 +278,8 @@
 
 lemma table_append_Some_iff: "table_of (xs@ys) k = Some z = 
  (table_of xs k = Some z \<or> (table_of xs k = None \<and> table_of ys k = Some z))"
-apply (simp only: map_of_override [THEN sym])
-apply (rule override_Some_iff)
+apply (simp)
+apply (rule map_add_Some_iff)
 done
 
 lemma table_of_filter_unique_SomeD [rule_format (no_asm)]: