# HG changeset patch
# User nipkow
# Date 1236636461 -3600
# Node ID 8f9793efe5f2414c1b7ae21ec9ff95c40bfb1a6f
# Parent  3934d42344e01f88951574e22bd9ed88606141c7
Docs

diff -r 3934d42344e0 -r 8f9793efe5f2 src/HOL/Docs/Main_Doc.thy
--- a/src/HOL/Docs/Main_Doc.thy	Mon Mar 09 14:20:07 2009 +0100
+++ b/src/HOL/Docs/Main_Doc.thy	Mon Mar 09 23:07:41 2009 +0100
@@ -1,5 +1,5 @@
 (*<*)
-theory MainDoc
+theory Main_Doc
 imports Main
 begin
 
@@ -56,7 +56,7 @@
 \section{Orderings}
 
 A collection of classes constraining @{text"\<le>"} and @{text"<"}:
-preorders, partial orders, linear orders, dense linear orders and wellorders.
+preorder, partial order, linear order, dense linear order and wellorder.
 
 \begin{tabular}{@ {} l @ {~::~} l @ {}}
 @{const Orderings.Least} & @{typeof Orderings.Least}\\
@@ -75,6 +75,33 @@
 @{term"LEAST x. P"} & @{term[source]"Least (\<lambda>x. P)"}\\
 \end{supertabular}
 
+
+\section{Lattices}
+
+Classes semilattice, lattice, distributive lattice and complete lattice (the
+latter in theory @{theory Set}).
+
+\begin{tabular}{@ {} l @ {~::~} l @ {}}
+@{const Lattices.inf} & @{typeof Lattices.inf}\\
+@{const Lattices.sup} & @{typeof Lattices.sup}\\
+@{const Set.Inf} & @{term_type_only Set.Inf "'a set \<Rightarrow> 'a::complete_lattice"}\\
+@{const Set.Sup} & @{term_type_only Set.Sup "'a set \<Rightarrow> 'a::complete_lattice"}\\
+\end{tabular}
+
+\subsubsection*{Syntax}
+
+Only available locally:
+
+\begin{supertabular}{@ {} l @ {\quad$\equiv$\quad} l @ {}}
+@{text[source]"x \<sqsubseteq> y"} & @{term"x \<le> y"}\\
+@{text[source]"x \<sqsubset> y"} & @{term"x < y"}\\
+@{text[source]"x \<sqinter> y"} & @{term"inf x y"}\\
+@{text[source]"x \<squnion> y"} & @{term"sup x y"}\\
+@{text[source]"\<Sqinter> A"} & @{term"Sup A"}\\
+@{text[source]"\<Squnion> A"} & @{term"Inf A"}\\
+\end{supertabular}
+
+
 \section{Set}
 
 Sets are predicates: @{text[source]"'a set  =  'a \<Rightarrow> bool"}
@@ -193,7 +220,7 @@
 
 \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>('c*'a)set\<Rightarrow>('c*'b)set"}\\
 @{const Relation.Image} & @{term_type_only Relation.Image "('a*'b)set\<Rightarrow>'a set\<Rightarrow>'b set"}\\
@@ -210,8 +237,8 @@
 @{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}
+@{const Relation.total} & @{term_type_only Relation.total "('a*'a)set\<Rightarrow>bool"}
+\end{tabular}
 
 \subsubsection*{Syntax}
 
@@ -324,6 +351,29 @@
 \end{tabular}
 
 
+\section{Finite\_Set}
+
+
+\begin{supertabular}{@ {} l @ {~::~} l @ {}}
+@{const Finite_Set.finite} & @{term_type_only Finite_Set.finite "'a set\<Rightarrow>bool"}\\
+@{const Finite_Set.card} & @{term_type_only Finite_Set.card "'a set => nat"}\\
+@{const Finite_Set.fold} & @{term_type_only Finite_Set.fold "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> 'a set \<Rightarrow> 'b"}\\
+@{const Finite_Set.fold_image} & @{typ "('b \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> 'a set \<Rightarrow> 'b"}\\
+@{const Finite_Set.setsum} & @{term_type_only Finite_Set.setsum "('a => 'b) => 'a set => 'b::comm_monoid_add"}\\
+@{const Finite_Set.setprod} & @{term_type_only Finite_Set.setprod "('a => 'b) => 'a set => 'b::comm_monoid_mult"}\\
+\end{supertabular}
+
+
+\subsubsection*{Syntax}
+
+\begin{supertabular}{@ {} l @ {\quad$\equiv$\quad} l @ {}}
+@{term"setsum (%x. x) A"} & @{term[source]"setsum (\<lambda>x. x) A"}\\
+@{term"setsum (%x. t) A"} & @{term[source]"setsum (\<lambda>x. t) A"}\\
+@{term[source]"\<Sum>x|P. t"} & @{term"\<Sum>x|P. t"}\\
+\multicolumn{2}{@ {}l@ {}}{Similarly for @{text"\<Prod>"} instead of @{text"\<Sum>"}}\\
+\end{supertabular}
+
+
 \section{Wellfounded}
 
 \begin{supertabular}{@ {} l @ {~::~} l @ {}}
diff -r 3934d42344e0 -r 8f9793efe5f2 src/HOL/Docs/ROOT.ML
--- a/src/HOL/Docs/ROOT.ML	Mon Mar 09 14:20:07 2009 +0100
+++ b/src/HOL/Docs/ROOT.ML	Mon Mar 09 23:07:41 2009 +0100
@@ -1,2 +1,2 @@
-use_thy "MainDoc";
+use_thy "Main_Doc";
 
diff -r 3934d42344e0 -r 8f9793efe5f2 src/HOL/Docs/document/root.tex
--- a/src/HOL/Docs/document/root.tex	Mon Mar 09 14:20:07 2009 +0100
+++ b/src/HOL/Docs/document/root.tex	Mon Mar 09 23:07:41 2009 +0100
@@ -4,7 +4,7 @@
 % further packages required for unusual symbols (see also
 % isabellesym.sty), use only when needed
 
-%\usepackage{amssymb}
+\usepackage{amssymb}
   %for \<leadsto>, \<box>, \<diamond>, \<sqsupset>, \<mho>, \<Join>,
   %\<lhd>, \<lesssim>, \<greatersim>, \<lessapprox>, \<greaterapprox>,
   %\<triangleq>, \<yen>, \<lozenge>
@@ -17,7 +17,7 @@
   %for \<onesuperior>, \<onequarter>, \<twosuperior>, \<onehalf>,
   %\<threesuperior>, \<threequarters>, \<degree>
 
-%\usepackage[only,bigsqcap]{stmaryrd}
+\usepackage[only,bigsqcap]{stmaryrd}
   %for \<Sqinter>
 
 %\usepackage{eufrak}
@@ -43,7 +43,7 @@
 \begin{document}
 
 \title{What's in Main}
-\author{}
+\author{Tobias Nipkow}
 \date{}
 \maketitle