# HG changeset patch
# User nipkow
# Date 1236637753 -3600
# Node ID 042641837e79de56e6d1db4d7a87d2c459cdd5c5
# Parent  c47e0189013b4f1650bc3974a610d0ef990fd2dc
Docs

diff -r c47e0189013b -r 042641837e79 src/HOL/Docs/Main_Doc.thy
--- a/src/HOL/Docs/Main_Doc.thy	Mon Mar 09 23:07:51 2009 +0100
+++ b/src/HOL/Docs/Main_Doc.thy	Mon Mar 09 23:29:13 2009 +0100
@@ -541,7 +541,7 @@
 \subsubsection*{Syntax}
 
 \begin{tabular}{@ {} l @ {\quad$\equiv$\quad} l @ {}}
-@{text"empty"} & @{term"\<lambda>x. None"}\\
+@{term"Map.empty"} & @{term"\<lambda>x. None"}\\
 @{term"m(x:=Some y)"} & @{term[source]"m(x:=Some y)"}\\
 @{text"m(x\<^isub>1\<mapsto>y\<^isub>1,\<dots>,x\<^isub>n\<mapsto>y\<^isub>n)"} & @{text[source]"m(x\<^isub>1\<mapsto>y\<^isub>1)\<dots>(x\<^isub>n\<mapsto>y\<^isub>n)"}\\
 @{term"map_upds m xs ys"} & @{term[source]"map_upds m xs ys"}\\