# HG changeset patch # User nipkow # Date 1676897456 -3600 # Node ID 0794ec39a4e0c103256fd741a174a21d3881f7a8 # Parent 334015f9098ed8187ea98945d653dafa231fc439 backout rev 334015f9098e (for Main_Doc.thy only) diff -r 334015f9098e -r 0794ec39a4e0 src/Doc/Main/Main_Doc.thy --- a/src/Doc/Main/Main_Doc.thy Tue Feb 14 08:10:17 2023 +0100 +++ b/src/Doc/Main/Main_Doc.thy Mon Feb 20 13:50:56 2023 +0100 @@ -543,7 +543,6 @@ \<^const>\List.list_all2\ & \<^typeof>\List.list_all2\\\ \<^const>\List.list_update\ & \<^typeof>\List.list_update\\\ \<^const>\List.map\ & \<^typeof>\List.map\\\ -\<^const>\List.map_of\ & \<^typeof>\List.map_of\\\ \<^const>\List.measures\ & @{term_type_only List.measures "('a\nat)list\('a*'a)set"}\\ \<^const>\List.nth\ & \<^typeof>\List.nth\\\ \<^const>\List.nths\ & \<^typeof>\List.nths\\\ @@ -586,31 +585,32 @@ qualifier \q\<^sub>i\ is either a generator \mbox{\pat \ e\} or a guard, i.e.\ boolean expression. -%\section*{Map} -% -%Maps model partial functions and are often used as finite tables. However, -%the domain of a map may be infinite. -% -%\begin{tabular}{@ {} l @ {~::~} l @ {}} -%\\Map.empty\ & \\Map.empty\\\ -%\\Map.map_add\ & \\Map.map_add\\\ -%\\Map.map_comp\ & \\Map.map_comp\\\ -%\\Map.restrict_map\ & @ {term_type_only Map.restrict_map "('a\'b option)\'a set\('a\'b option)"}\\ -%\\Map.dom\ & @{term_type_only Map.dom "('a\'b option)\'a set"}\\ -%\\Map.ran\ & @{term_type_only Map.ran "('a\'b option)\'b set"}\\ -%\\Map.map_le\ & \\Map.map_le\\\ -%\\Map.map_upds\ & \\Map.map_upds\\\ -%\end{tabular} -% -%\subsubsection*{Syntax} -% -%\begin{tabular}{@ {} l @ {\quad$\equiv$\quad} l @ {}} -%\\Map.empty\ & @ {term[source] "\_. None"}\\ -%\\m(x:=Some y)\ & @ {term[source]"m(x:=Some y)"}\\ -%m(x1\y1,\,xn\yn) & @ {text[source]"m(x1\y1)\(xn\yn)"}\\ -%[x1\y1,\,xn\yn] & @ {text[source]"Map.empty(x1\y1,\,xn\yn)"}\\ -%\\map_upds m xs ys\ & @ {term[source]"map_upds m xs ys"}\\ -%\end{tabular} +\section*{Map} + +Maps model partial functions and are often used as finite tables. However, +the domain of a map may be infinite. + +\begin{tabular}{@ {} l @ {~::~} l @ {}} +\<^const>\Map.empty\ & \<^typeof>\Map.empty\\\ +\<^const>\Map.map_add\ & \<^typeof>\Map.map_add\\\ +\<^const>\Map.map_comp\ & \<^typeof>\Map.map_comp\\\ +\<^const>\Map.restrict_map\ & @{term_type_only Map.restrict_map "('a\'b option)\'a set\('a\'b option)"}\\ +\<^const>\Map.dom\ & @{term_type_only Map.dom "('a\'b option)\'a set"}\\ +\<^const>\Map.ran\ & @{term_type_only Map.ran "('a\'b option)\'b set"}\\ +\<^const>\Map.map_le\ & \<^typeof>\Map.map_le\\\ +\<^const>\Map.map_of\ & \<^typeof>\Map.map_of\\\ +\<^const>\Map.map_upds\ & \<^typeof>\Map.map_upds\\\ +\end{tabular} + +\subsubsection*{Syntax} + +\begin{tabular}{@ {} l @ {\quad$\equiv$\quad} l @ {}} +\<^term>\Map.empty\ & @{term[source] "\_. None"}\\ +\<^term>\m(x:=Some y)\ & @{term[source]"m(x:=Some y)"}\\ +\m(x\<^sub>1\y\<^sub>1,\,x\<^sub>n\y\<^sub>n)\ & @{text[source]"m(x\<^sub>1\y\<^sub>1)\(x\<^sub>n\y\<^sub>n)"}\\ +\[x\<^sub>1\y\<^sub>1,\,x\<^sub>n\y\<^sub>n]\ & @{text[source]"Map.empty(x\<^sub>1\y\<^sub>1,\,x\<^sub>n\y\<^sub>n)"}\\ +\<^term>\map_upds m xs ys\ & @{term[source]"map_upds m xs ys"}\\ +\end{tabular} \section*{Infix operators in Main} % \<^theory>\Main\