# HG changeset patch
# User nipkow
# Date 1236768074 -3600
# Node ID 193cf2fa692a3feba8902bf2d853944c59db66ab
# Parent  57c68b3af2eae3dbd04d823fbb91e18640471c9f# Parent  5f47d3cb781a63f3b0b9c27906a28a8e2d596c5e
merged

diff -r 57c68b3af2ea -r 193cf2fa692a src/HOL/Docs/Main_Doc.thy
--- a/src/HOL/Docs/Main_Doc.thy	Wed Mar 11 10:58:18 2009 +0100
+++ b/src/HOL/Docs/Main_Doc.thy	Wed Mar 11 11:41:14 2009 +0100
@@ -23,57 +23,50 @@
 
 \section{HOL}
 
-The basic logic: @{prop "x = y"}, @{const True}, @{const False}, @{prop"Not P"}, @{prop"P & Q"}, @{prop "P | Q"}, @{prop "P --> Q"}, @{prop"ALL x. P"}, @{prop"EX x. P"}, @{prop"EX! x. P"}, @{term"THE x. P"}. (\textsc{ascii}: \verb$~$, \verb$&$, \verb$|$, \verb$-->$, \texttt{ALL}, \texttt{EX})
+The basic logic: @{prop "x = y"}, @{const True}, @{const False}, @{prop"Not P"}, @{prop"P & Q"}, @{prop "P | Q"}, @{prop "P --> Q"}, @{prop"ALL x. P"}, @{prop"EX x. P"}, @{prop"EX! x. P"}, @{term"THE x. P"}.
+\smallskip
+
+\begin{tabular}{@ {} l @ {~::~} l @ {}}
+@{const HOL.undefined} & @{typeof HOL.undefined}\\
+@{const HOL.default} & @{typeof HOL.default}\\
+\end{tabular}
+
+\subsubsection*{Syntax}
 
-Overloaded operators:
+\begin{supertabular}{@ {} l @ {\quad$\equiv$\quad} l l @ {}}
+@{term"~(x = y)"} & @{term[source]"\<not> (x = y)"} & (\verb$~=$)\\
+@{term[source]"P \<longleftrightarrow> Q"} & @{term"P \<longleftrightarrow> Q"} \\
+@{term"If x y z"} & @{term[source]"If x y z"}\\
+@{term"Let e\<^isub>1 (%x. e\<^isub>2)"} & @{term[source]"Let e\<^isub>1 (\<lambda>x. e\<^isub>2)"}\\
+\end{supertabular}
+
+
+\section{Orderings}
+
+A collection of classes defining basic orderings:
+preorder, partial order, linear order, dense linear order and wellorder.
+\smallskip
 
 \begin{supertabular}{@ {} l @ {~::~} l l @ {}}
-@{text "0"} & @{typeof HOL.zero}\\
-@{text "1"} & @{typeof HOL.one}\\
-@{const HOL.plus} & @{typeof HOL.plus}\\
-@{const HOL.minus} & @{typeof HOL.minus}\\
-@{const HOL.uminus} & @{typeof HOL.uminus}\\
-@{const HOL.times} & @{typeof HOL.times}\\
-@{const HOL.inverse} & @{typeof HOL.inverse}\\
-@{const HOL.divide} & @{typeof HOL.divide}\\
-@{const HOL.abs} & @{typeof HOL.abs}\\
-@{const HOL.sgn} & @{typeof HOL.sgn}\\
 @{const HOL.less_eq} & @{typeof HOL.less_eq} & (\verb$<=$)\\
 @{const HOL.less} & @{typeof HOL.less}\\
-@{const HOL.default} & @{typeof HOL.default}\\
-@{const HOL.undefined} & @{typeof HOL.undefined}\\
+@{const Orderings.Least} & @{typeof Orderings.Least}\\
+@{const Orderings.min} & @{typeof Orderings.min}\\
+@{const Orderings.max} & @{typeof Orderings.max}\\
+@{const[source] top} & @{typeof Orderings.top}\\
+@{const[source] bot} & @{typeof Orderings.bot}\\
+@{const Orderings.mono} & @{typeof Orderings.mono}\\
+@{const Orderings.strict_mono} & @{typeof Orderings.strict_mono}\\
 \end{supertabular}
 
 \subsubsection*{Syntax}
 
-\begin{supertabular}{@ {} l @ {\quad$\equiv$\quad} l @ {}}
-@{term"~(x = y)"} & @{term[source]"\<not> (x = y)"}\\
-@{term[source]"P \<longleftrightarrow> Q"} & @{term"P \<longleftrightarrow> Q"}\\
-@{term"If x y z"} & @{term[source]"If x y z"}\\
-@{term"Let e\<^isub>1 (%x. e\<^isub>2)"} & @{term[source]"Let e\<^isub>1 (\<lambda>x. e\<^isub>2)"}\\
-@{term"abs x"} & @{term[source]"abs x"}\\
-@{term"uminus x"} & @{term[source]"uminus x"}\\
-\end{supertabular}
-
-\section{Orderings}
-
-A collection of classes constraining @{text"\<le>"} and @{text"<"}:
-preorder, partial order, linear order, dense linear order and wellorder.
-
-\begin{tabular}{@ {} l @ {~::~} l @ {}}
-@{const Orderings.Least} & @{typeof Orderings.Least}\\
-@{const Orderings.min} & @{typeof Orderings.min}\\
-@{const Orderings.max} & @{typeof Orderings.max}\\
-@{const Orderings.mono} & @{typeof Orderings.mono}\\
-\end{tabular}
-
-\subsubsection*{Syntax}
-
-\begin{supertabular}{@ {} l @ {\quad$\equiv$\quad} l @ {}}
-@{term[source]"x \<ge> y"} & @{term"x \<ge> y"}\\
+\begin{supertabular}{@ {} l @ {\quad$\equiv$\quad} l l @ {}}
+@{term[source]"x \<ge> y"} & @{term"x \<ge> y"} & (\verb$>=$)\\
 @{term[source]"x > y"} & @{term"x > y"}\\
 @{term"ALL x<=y. P"} & @{term[source]"\<forall>x. x \<le> y \<longrightarrow> P"}\\
-\multicolumn{2}{@ {}l@ {}}{Similarly for $<$, $\ge$ and $>$, and for @{text"\<exists>"}}\\
+@{term"EX x<=y. P"} & @{term[source]"\<exists>x. x \<le> y \<and> P"}\\
+\multicolumn{2}{@ {}l@ {}}{Similarly for $<$, $\ge$ and $>$}\\
 @{term"LEAST x. P"} & @{term[source]"Least (\<lambda>x. P)"}\\
 \end{supertabular}
 
@@ -92,7 +85,8 @@
 
 \subsubsection*{Syntax}
 
-Only available locally:
+Available by loading theory @{text Lattice_Syntax} in directory @{text
+Library}.
 
 \begin{supertabular}{@ {} l @ {\quad$\equiv$\quad} l @ {}}
 @{text[source]"x \<sqsubseteq> y"} & @{term"x \<le> y"}\\
@@ -101,6 +95,8 @@
 @{text[source]"x \<squnion> y"} & @{term"sup x y"}\\
 @{text[source]"\<Sqinter> A"} & @{term"Sup A"}\\
 @{text[source]"\<Squnion> A"} & @{term"Inf A"}\\
+@{text[source]"\<top>"} & @{term[source] top}\\
+@{text[source]"\<bottom>"} & @{term[source] bot}\\
 \end{supertabular}
 
 
@@ -136,7 +132,7 @@
 @{term"A \<subset> B"} & @{term[source]"A < B"}\\
 @{term[source]"A \<supseteq> B"} & @{term[source]"B \<le> A"}\\
 @{term[source]"A \<supset> B"} & @{term[source]"B < A"}\\
-@{term"{x. P}"} & @{term[source]"Collect(\<lambda>x. P)"}\\
+@{term"{x. P}"} & @{term[source]"Collect (\<lambda>x. P)"}\\
 @{term[mode=xsymbols]"UN x:I. A"} & @{term[source]"UNION I (\<lambda>x. A)"} & (\texttt{UN})\\
 @{term[mode=xsymbols]"UN x. A"} & @{term[source]"UNION UNIV (\<lambda>x. A)"}\\
 @{term[mode=xsymbols]"INT x:I. A"} & @{term[source]"INTER I (\<lambda>x. A)"} & (\texttt{INT})\\
@@ -203,26 +199,26 @@
 @{const snd} & @{typeof snd}\\
 @{const split} & @{typeof split}\\
 @{const curry} & @{typeof curry}\\
-@{const Product_Type.Times} & @{typeof Product_Type.Times}\\
 @{const Product_Type.Sigma} & @{term_type_only Product_Type.Sigma "'a set\<Rightarrow>('a\<Rightarrow>'b set)\<Rightarrow>('a*'b)set"}\\
 \end{supertabular}
 
 \subsubsection*{Syntax}
 
-\begin{tabular}{@ {} l @ {\quad$\equiv$\quad} l @ {}}
+\begin{tabular}{@ {} l @ {\quad$\equiv$\quad} ll @ {}}
 @{term"Pair a b"} & @{term[source]"Pair a b"}\\
 @{term"split (\<lambda>x y. t)"} & @{term[source]"split (\<lambda>x y. t)"}\\
+@{term"A <*> B"} &  @{text"Sigma A (\<lambda>\<^raw:\_>. B)"} & (\verb$<*>$)
 \end{tabular}
 
 Pairs may be nested. Nesting to the right is printed as a tuple,
-e.g.\ \mbox{@{term"(a,b,c)"}} is really @{text"(a,(b,c))"}.
+e.g.\ \mbox{@{term"(a,b,c)"}} is really \mbox{@{text"(a, (b, c))"}.}
 Pattern matching with pairs and tuples extends to all binders,
-e.g.\ @{prop"ALL (x,y):A. P"}, @{term"{(x,y). P}"}, etc.
+e.g.\ \mbox{@{prop"ALL (x,y):A. P"},} @{term"{(x,y). P}"}, etc.
 
 
 \section{Relation}
 
-\begin{tabular}{@ {} l @ {~::~} l @ {}}
+\begin{supertabular}{@ {} 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"}\\
@@ -239,13 +235,13 @@
 @{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{tabular}
+@{const Relation.total} & @{term_type_only Relation.total "('a*'a)set\<Rightarrow>bool"}\\
+\end{supertabular}
 
 \subsubsection*{Syntax}
 
-\begin{tabular}{@ {} l @ {\quad$\equiv$\quad} l @ {}}
-@{term"converse r"} & @{term[source]"converse r"}
+\begin{tabular}{@ {} l @ {\quad$\equiv$\quad} l l @ {}}
+@{term"converse r"} & @{term[source]"converse r"} & (\verb$^-1$)
 \end{tabular}
 
 \section{Equiv\_Relations}
@@ -276,19 +272,41 @@
 
 \subsubsection*{Syntax}
 
-\begin{tabular}{@ {} l @ {\quad$\equiv$\quad} l @ {}}
-@{term"rtrancl r"} & @{term[source]"rtrancl r"}\\
-@{term"trancl r"} & @{term[source]"trancl r"}\\
-@{term"reflcl r"} & @{term[source]"reflcl r"}
+\begin{tabular}{@ {} l @ {\quad$\equiv$\quad} l l @ {}}
+@{term"rtrancl r"} & @{term[source]"rtrancl r"} & (\verb$^*$)\\
+@{term"trancl r"} & @{term[source]"trancl r"} & (\verb$^+$)\\
+@{term"reflcl r"} & @{term[source]"reflcl r"} & (\verb$^=$)
 \end{tabular}
 
 
 \section{Algebra}
 
-Theories @{theory OrderedGroup} and @{theory Ring_and_Field} define a large
-collection of classes describing common algebraic structures from semigroups
-up to fields. Everything is done in terms of @{const plus}, @{const times}
-and other overloaded operators.
+Theories @{theory OrderedGroup}, @{theory Ring_and_Field} and @{theory
+Divides} define a large collection of classes describing common algebraic
+structures from semigroups up to fields. Everything is done in terms of
+overloaded operators:
+
+\begin{supertabular}{@ {} l @ {~::~} l l @ {}}
+@{text "0"} & @{typeof zero}\\
+@{text "1"} & @{typeof one}\\
+@{const plus} & @{typeof plus}\\
+@{const minus} & @{typeof minus}\\
+@{const uminus} & @{typeof uminus} & (\verb$-$)\\
+@{const times} & @{typeof times}\\
+@{const inverse} & @{typeof inverse}\\
+@{const divide} & @{typeof divide}\\
+@{const abs} & @{typeof abs}\\
+@{const sgn} & @{typeof sgn}\\
+@{const dvd_class.dvd} & @{typeof "dvd_class.dvd"}\\
+@{const div_class.div} & @{typeof "div_class.div"}\\
+@{const div_class.mod} & @{typeof "div_class.mod"}\\
+\end{supertabular}
+
+\subsubsection*{Syntax}
+
+\begin{tabular}{@ {} l @ {\quad$\equiv$\quad} l @ {}}
+@{term"abs x"} & @{term[source]"abs x"}
+\end{tabular}
 
 
 \section{Nat}
@@ -340,10 +358,10 @@
 @{term "sgn :: int \<Rightarrow> int"}\\
 \end{tabular}
 
-\begin{tabular}{@ {} l @ {~::~} l @ {}}
+\begin{tabular}{@ {} l @ {~::~} l l @ {}}
 @{const Int.nat} & @{typeof Int.nat}\\
 @{const Int.of_int} & @{typeof Int.of_int}\\
-@{const Int.Ints} & @{term_type_only Int.Ints "'a::ring_1 set"}\\
+@{const Int.Ints} & @{term_type_only Int.Ints "'a::ring_1 set"} & (\verb$Ints$)
 \end{tabular}
 
 \subsubsection*{Syntax}
@@ -368,11 +386,11 @@
 
 \subsubsection*{Syntax}
 
-\begin{supertabular}{@ {} l @ {\quad$\equiv$\quad} l @ {}}
-@{term"setsum (%x. x) A"} & @{term[source]"setsum (\<lambda>x. x) A"}\\
+\begin{supertabular}{@ {} l @ {\quad$\equiv$\quad} l l @ {}}
+@{term"setsum (%x. x) A"} & @{term[source]"setsum (\<lambda>x. x) A"} & (\verb$SUM$)\\
 @{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>"}}\\
+\multicolumn{2}{@ {}l@ {}}{Similarly for @{text"\<Prod>"} instead of @{text"\<Sum>"}} & (\verb$PROD$)\\
 \end{supertabular}
 
 
@@ -514,8 +532,8 @@
 \end{supertabular}
 \medskip
 
-Comprehension: @{text"[e. q\<^isub>1, \<dots>, q\<^isub>n]"} where each
-qualifier @{text q\<^isub>i} is either a generator @{text"pat \<leftarrow> e"} or a
+List comprehension: @{text"[e. q\<^isub>1, \<dots>, q\<^isub>n]"} where each
+qualifier @{text q\<^isub>i} is either a generator \mbox{@{text"pat \<leftarrow> e"}} or a
 guard, i.e.\ boolean expression.
 
 \section{Map}
@@ -544,6 +562,7 @@
 @{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)"}\\
+@{text"[x\<^isub>1\<mapsto>y\<^isub>1,\<dots>,x\<^isub>n\<mapsto>y\<^isub>n]"} & @{text[source]"Map.empty(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"}\\
 \end{tabular}
 
diff -r 57c68b3af2ea -r 193cf2fa692a src/HOL/Docs/ROOT.ML
--- a/src/HOL/Docs/ROOT.ML	Wed Mar 11 10:58:18 2009 +0100
+++ b/src/HOL/Docs/ROOT.ML	Wed Mar 11 11:41:14 2009 +0100
@@ -1,2 +1,1 @@
 use_thy "Main_Doc";
-
diff -r 57c68b3af2ea -r 193cf2fa692a src/HOL/Docs/document/root.tex
--- a/src/HOL/Docs/document/root.tex	Wed Mar 11 10:58:18 2009 +0100
+++ b/src/HOL/Docs/document/root.tex	Wed Mar 11 11:41:14 2009 +0100
@@ -1,4 +1,13 @@
-\documentclass[11pt,a4paper]{article}
+\documentclass[12pt,a4paper]{article}
+
+\oddsidemargin=4.6mm
+\evensidemargin=4.6mm
+\textwidth=150mm
+\topmargin=4.6mm
+\headheight=0mm
+\headsep=0mm
+\textheight=234mm
+
 \usepackage{isabelle,isabellesym}
 
 % further packages required for unusual symbols (see also
diff -r 57c68b3af2ea -r 193cf2fa692a src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Wed Mar 11 10:58:18 2009 +0100
+++ b/src/HOL/IsaMakefile	Wed Mar 11 11:41:14 2009 +0100
@@ -692,7 +692,7 @@
 
 $(LOG)/HOL-Docs.gz: $(OUT)/HOL Docs/Main_Doc.thy Docs/ROOT.ML	\
   Docs/document/root.tex
-	@$(ISABELLE_TOOL) usedir $(OUT)/HOL Docs
+	@$(ISABELLE_TOOL) usedir -D generated $(OUT)/HOL Docs
 
 
 ## HOL-Lambda