# HG changeset patch # User nipkow # Date 1255547693 -7200 # Node ID ba14400f7f34772b7f3322febcbf9ae35c52bed3 # Parent f24fd64d27a2a0e691c53df4e9ba0e901d7cabbe added List.nth diff -r f24fd64d27a2 -r ba14400f7f34 doc-src/Main/Docs/Main_Doc.thy --- a/doc-src/Main/Docs/Main_Doc.thy Wed Oct 14 16:45:26 2009 +0200 +++ b/doc-src/Main/Docs/Main_Doc.thy Wed Oct 14 21:14:53 2009 +0200 @@ -145,9 +145,9 @@ \section{Fun} -\begin{supertabular}{@ {} l @ {~::~} l @ {}} +\begin{supertabular}{@ {} l @ {~::~} l l @ {}} @{const "Fun.id"} & @{typeof Fun.id}\\ -@{const "Fun.comp"} & @{typeof Fun.comp}\\ +@{const "Fun.comp"} & @{typeof Fun.comp} & (\texttt{o})\\ @{const "Fun.inj_on"} & @{term_type_only Fun.inj_on "('a\'b)\'a set\bool"}\\ @{const "Fun.inj"} & @{typeof Fun.inj}\\ @{const "Fun.surj"} & @{typeof Fun.surj}\\ @@ -493,6 +493,7 @@ @{const List.list_update} & @{typeof List.list_update}\\ @{const List.map} & @{typeof List.map}\\ @{const List.measures} & @{term_type_only List.measures "('a\nat)list\('a*'a)set"}\\ +@{const List.nth} & @{typeof List.nth}\\ @{const List.remdups} & @{typeof List.remdups}\\ @{const List.removeAll} & @{typeof List.removeAll}\\ @{const List.remove1} & @{typeof List.remove1}\\ diff -r f24fd64d27a2 -r ba14400f7f34 doc-src/Main/Docs/document/Main_Doc.tex --- a/doc-src/Main/Docs/document/Main_Doc.tex Wed Oct 14 16:45:26 2009 +0200 +++ b/doc-src/Main/Docs/document/Main_Doc.tex Wed Oct 14 21:14:53 2009 +0200 @@ -156,9 +156,9 @@ \section{Fun} -\begin{supertabular}{@ {} l @ {~::~} l @ {}} +\begin{supertabular}{@ {} l @ {~::~} l l @ {}} \isa{id} & \isa{{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a}\\ -\isa{op\ {\isasymcirc}} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}b{\isacharparenright}\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}c\ {\isasymRightarrow}\ {\isacharprime}a{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}c\ {\isasymRightarrow}\ {\isacharprime}b}\\ +\isa{op\ {\isasymcirc}} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}b{\isacharparenright}\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}c\ {\isasymRightarrow}\ {\isacharprime}a{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}c\ {\isasymRightarrow}\ {\isacharprime}b} & (\texttt{o})\\ \isa{inj{\isacharunderscore}on} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}b{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ set\ {\isasymRightarrow}\ bool}\\ \isa{inj} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}b{\isacharparenright}\ {\isasymRightarrow}\ bool}\\ \isa{surj} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}b{\isacharparenright}\ {\isasymRightarrow}\ bool}\\ @@ -503,6 +503,7 @@ \isa{list{\isacharunderscore}update} & \isa{{\isacharprime}a\ list\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ list}\\ \isa{map} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}b{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}b\ list}\\ \isa{measures} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ nat{\isacharparenright}\ list\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}\ set}\\ +\isa{op\ {\isacharbang}} & \isa{{\isacharprime}a\ list\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ {\isacharprime}a}\\ \isa{remdups} & \isa{{\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list}\\ \isa{removeAll} & \isa{{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list}\\ \isa{remove{\isadigit{1}}} & \isa{{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list}\\