doc-src/Main/Docs/Main_Doc.thy

 \end{supertabular}
 
 
 \section{Set}
 
-Sets are predicates: @{text[source]"'a set  =  'a \<Rightarrow> bool"}
-\bigskip
+%Sets are predicates: @{text[source]"'a set  =  'a \<Rightarrow> bool"}
+%\bigskip
 
 \begin{supertabular}{@ {} l @ {~::~} l l @ {}}
 @{const Set.empty} & @{term_type_only "Set.empty" "'a set"}\\
 @{const Set.insert} & @{term_type_only insert "'a\<Rightarrow>'a set\<Rightarrow>'a set"}\\
 @{const Collect} & @{term_type_only Collect "('a\<Rightarrow>bool)\<Rightarrow>'a set"}\\

 e.g.\ \mbox{@{prop"ALL (x,y):A. P"},} @{term"{(x,y). P}"}, etc.
 
 
 \section{Relation}
 
-\begin{supertabular}{@ {} l @ {~::~} l @ {}}
+\begin{tabular}{@ {} l @ {~::~} l @ {}}
 @{const Relation.converse} & @{term_type_only Relation.converse "('a * 'b)set \<Rightarrow> ('b*'a)set"}\\
 @{const Relation.rel_comp} & @{term_type_only Relation.rel_comp "('a*'b)set\<Rightarrow>('b*'c)set\<Rightarrow>('a*'c)set"}\\
 @{const Relation.Image} & @{term_type_only Relation.Image "('a*'b)set\<Rightarrow>'a set\<Rightarrow>'b set"}\\
 @{const Relation.inv_image} & @{term_type_only Relation.inv_image "('a*'a)set\<Rightarrow>('b\<Rightarrow>'a)\<Rightarrow>('b*'b)set"}\\
 @{const Relation.Id_on} & @{term_type_only Relation.Id_on "'a set\<Rightarrow>('a*'a)set"}\\

 @{const Relation.antisym} & @{term_type_only Relation.antisym "('a*'a)set\<Rightarrow>bool"}\\
 @{const Relation.trans} & @{term_type_only Relation.trans "('a*'a)set\<Rightarrow>bool"}\\
 @{const Relation.irrefl} & @{term_type_only Relation.irrefl "('a*'a)set\<Rightarrow>bool"}\\
 @{const Relation.total_on} & @{term_type_only Relation.total_on "'a set\<Rightarrow>('a*'a)set\<Rightarrow>bool"}\\
 @{const Relation.total} & @{term_type_only Relation.total "('a*'a)set\<Rightarrow>bool"}\\
-\end{supertabular}
+\end{tabular}
 
 \subsubsection*{Syntax}
 
 \begin{tabular}{@ {} l @ {\quad$\equiv$\quad} l l @ {}}
 @{term"converse r"} & @{term[source]"converse r"} & (\verb$^-1$)
 \end{tabular}
+\medskip
+
+\noindent
+Type synonym @{typ"'a rel"} @{text"="} @{typ "('a * 'a)set"}
 
 \section{Equiv\_Relations}
 
 \begin{supertabular}{@ {} l @ {~::~} l @ {}}
 @{const Equiv_Relations.equiv} & @{term_type_only Equiv_Relations.equiv "'a set \<Rightarrow> ('a*'a)set\<Rightarrow>bool"}\\

 
 \begin{tabular}{@ {} lllllll @ {}}
 @{term "op + :: nat \<Rightarrow> nat \<Rightarrow> nat"} &
 @{term "op - :: nat \<Rightarrow> nat \<Rightarrow> nat"} &
 @{term "op * :: nat \<Rightarrow> nat \<Rightarrow> nat"} &
+@{term "op ^ :: nat \<Rightarrow> nat \<Rightarrow> nat"} &
 @{term "op div :: nat \<Rightarrow> nat \<Rightarrow> nat"}&
 @{term "op mod :: nat \<Rightarrow> nat \<Rightarrow> nat"}&
 @{term "op dvd :: nat \<Rightarrow> nat \<Rightarrow> bool"}\\
 @{term "op \<le> :: nat \<Rightarrow> nat \<Rightarrow> bool"} &
 @{term "op < :: nat \<Rightarrow> nat \<Rightarrow> bool"} &

 @{const List.concat} & @{typeof List.concat}\\
 @{const List.distinct} & @{typeof List.distinct}\\
 @{const List.drop} & @{typeof List.drop}\\
 @{const List.dropWhile} & @{typeof List.dropWhile}\\
 @{const List.filter} & @{typeof List.filter}\\
+@{const List.find} & @{typeof List.find}\\
 @{const List.fold} & @{typeof List.fold}\\
 @{const List.foldr} & @{typeof List.foldr}\\
 @{const List.foldl} & @{typeof List.foldl}\\
 @{const List.hd} & @{typeof List.hd}\\
 @{const List.last} & @{typeof List.last}\\

 \section{Map}
 
 Maps model partial functions and are often used as finite tables. However,
 the domain of a map may be infinite.
 
-@{text"'a \<rightharpoonup> 'b  =  'a \<Rightarrow> 'b option"}
-\bigskip
-
 \begin{supertabular}{@ {} 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\<Rightarrow>'b option)\<Rightarrow>'a set\<Rightarrow>('a\<Rightarrow>'b option)"}\\