# HG changeset patch
# User bulwahn
# Date 1323874591 -3600
# Node ID bce0a2089dfbd792b06613b27b8a7352c2048b31
# Parent  e62b319c76963b2681b5f1e289b780f2b4dd5d3a
fixed typo in theorem name in AList theory

diff -r e62b319c7696 -r bce0a2089dfb src/HOL/Library/AList.thy
--- a/src/HOL/Library/AList.thy	Wed Dec 14 15:56:29 2011 +0100
+++ b/src/HOL/Library/AList.thy	Wed Dec 14 15:56:31 2011 +0100
@@ -274,7 +274,7 @@
  "map_of (update x y (restrict D al)) = map_of (update x y (restrict (D-{x}) al))"
   by (simp add: update_conv' restr_conv') (rule fun_upd_restrict)
 
-lemma upate_restr_conv [simp]:
+lemma update_restr_conv [simp]:
  "x \<in> D \<Longrightarrow> 
  map_of (update x y (restrict D al)) = map_of (update x y (restrict (D-{x}) al))"
   by (simp add: update_conv' restr_conv')