more standard document preparation within session context;

--- a/doc-src/Main/Docs/Main_Doc.thy	Mon Aug 27 21:19:16 2012 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,596 +0,0 @@
-(*<*)
-theory Main_Doc
-imports Main
-begin
-
-setup {*
-  let
-    fun pretty_term_type_only ctxt (t, T) =
-      (if fastype_of t = Sign.certify_typ (Proof_Context.theory_of ctxt) T then ()
-       else error "term_type_only: type mismatch";
-       Syntax.pretty_typ ctxt T)
-  in
-    Thy_Output.antiquotation @{binding term_type_only}
-      (Args.term -- Args.typ_abbrev)
-      (fn {source, context = ctxt, ...} => fn arg =>
-        Thy_Output.output ctxt
-          (Thy_Output.maybe_pretty_source pretty_term_type_only ctxt source [arg]))
-  end
-*}
-setup {*
-  Thy_Output.antiquotation @{binding expanded_typ} (Args.typ >> single)
-    (fn {source, context, ...} => Thy_Output.output context o
-      Thy_Output.maybe_pretty_source Syntax.pretty_typ context source)
-*}
-(*>*)
-text{*
-
-\begin{abstract}
-This document lists the main types, functions and syntax provided by theory @{theory Main}. It is meant as a quick overview of what is available. The sophisticated class structure is only hinted at. For details see \url{http://isabelle.in.tum.de/library/HOL/}.
-\end{abstract}
-
-\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"}.
-\smallskip
-
-\begin{tabular}{@ {} l @ {~::~} l @ {}}
-@{const HOL.undefined} & @{typeof HOL.undefined}\\
-@{const HOL.default} & @{typeof HOL.default}\\
-\end{tabular}
-
-\subsubsection*{Syntax}
-
-\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 @ {}}
-@{const Orderings.less_eq} & @{typeof Orderings.less_eq} & (\verb$<=$)\\
-@{const Orderings.less} & @{typeof Orderings.less}\\
-@{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 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"}\\
-@{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}
-
-
-\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 Complete_Lattices.Inf} & @{term_type_only Complete_Lattices.Inf "'a set \<Rightarrow> 'a::Inf"}\\
-@{const Complete_Lattices.Sup} & @{term_type_only Complete_Lattices.Sup "'a set \<Rightarrow> 'a::Sup"}\\
-\end{tabular}
-
-\subsubsection*{Syntax}
-
-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"}\\
-@{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"}\\
-@{text[source]"\<top>"} & @{term[source] top}\\
-@{text[source]"\<bottom>"} & @{term[source] bot}\\
-\end{supertabular}
-
-
-\section{Set}
-
-%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"}\\
-@{const Set.member} & @{term_type_only Set.member "'a\<Rightarrow>'a set\<Rightarrow>bool"} & (\texttt{:})\\
-@{const Set.union} & @{term_type_only Set.union "'a set\<Rightarrow>'a set \<Rightarrow> 'a set"} & (\texttt{Un})\\
-@{const Set.inter} & @{term_type_only Set.inter "'a set\<Rightarrow>'a set \<Rightarrow> 'a set"} & (\texttt{Int})\\
-@{const UNION} & @{term_type_only UNION "'a set\<Rightarrow>('a \<Rightarrow> 'b set) \<Rightarrow> 'b set"}\\
-@{const INTER} & @{term_type_only INTER "'a set\<Rightarrow>('a \<Rightarrow> 'b set) \<Rightarrow> 'b set"}\\
-@{const Union} & @{term_type_only Union "'a set set\<Rightarrow>'a set"}\\
-@{const Inter} & @{term_type_only Inter "'a set set\<Rightarrow>'a set"}\\
-@{const Pow} & @{term_type_only Pow "'a set \<Rightarrow>'a set set"}\\
-@{const UNIV} & @{term_type_only UNIV "'a set"}\\
-@{const image} & @{term_type_only image "('a\<Rightarrow>'b)\<Rightarrow>'a set\<Rightarrow>'b set"}\\
-@{const Ball} & @{term_type_only Ball "'a set\<Rightarrow>('a\<Rightarrow>bool)\<Rightarrow>bool"}\\
-@{const Bex} & @{term_type_only Bex "'a set\<Rightarrow>('a\<Rightarrow>bool)\<Rightarrow>bool"}\\
-\end{supertabular}
-
-\subsubsection*{Syntax}
-
-\begin{supertabular}{@ {} l @ {\quad$\equiv$\quad} l l @ {}}
-@{text"{x\<^isub>1,\<dots>,x\<^isub>n}"} & @{text"insert x\<^isub>1 (\<dots> (insert x\<^isub>n {})\<dots>)"}\\
-@{term"x ~: A"} & @{term[source]"\<not>(x \<in> A)"}\\
-@{term"A \<subseteq> B"} & @{term[source]"A \<le> B"}\\
-@{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[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})\\
-@{term[mode=xsymbols]"INT x. A"} & @{term[source]"INTER UNIV (\<lambda>x. A)"}\\
-@{term"ALL x:A. P"} & @{term[source]"Ball A (\<lambda>x. P)"}\\
-@{term"EX x:A. P"} & @{term[source]"Bex A (\<lambda>x. P)"}\\
-@{term"range f"} & @{term[source]"f ` UNIV"}\\
-\end{supertabular}
-
-
-\section{Fun}
-
-\begin{supertabular}{@ {} l @ {~::~} l l @ {}}
-@{const "Fun.id"} & @{typeof Fun.id}\\
-@{const "Fun.comp"} & @{typeof Fun.comp} & (\texttt{o})\\
-@{const "Fun.inj_on"} & @{term_type_only Fun.inj_on "('a\<Rightarrow>'b)\<Rightarrow>'a set\<Rightarrow>bool"}\\
-@{const "Fun.inj"} & @{typeof Fun.inj}\\
-@{const "Fun.surj"} & @{typeof Fun.surj}\\
-@{const "Fun.bij"} & @{typeof Fun.bij}\\
-@{const "Fun.bij_betw"} & @{term_type_only Fun.bij_betw "('a\<Rightarrow>'b)\<Rightarrow>'a set\<Rightarrow>'b set\<Rightarrow>bool"}\\
-@{const "Fun.fun_upd"} & @{typeof Fun.fun_upd}\\
-\end{supertabular}
-
-\subsubsection*{Syntax}
-
-\begin{tabular}{@ {} l @ {\quad$\equiv$\quad} l @ {}}
-@{term"fun_upd f x y"} & @{term[source]"fun_upd f x y"}\\
-@{text"f(x\<^isub>1:=y\<^isub>1,\<dots>,x\<^isub>n:=y\<^isub>n)"} & @{text"f(x\<^isub>1:=y\<^isub>1)\<dots>(x\<^isub>n:=y\<^isub>n)"}\\
-\end{tabular}
-
-
-\section{Hilbert\_Choice}
-
-Hilbert's selection ($\varepsilon$) operator: @{term"SOME x. P"}.
-\smallskip
-
-\begin{tabular}{@ {} l @ {~::~} l @ {}}
-@{const Hilbert_Choice.inv_into} & @{term_type_only Hilbert_Choice.inv_into "'a set \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> ('b \<Rightarrow> 'a)"}
-\end{tabular}
-
-\subsubsection*{Syntax}
-
-\begin{tabular}{@ {} l @ {\quad$\equiv$\quad} l @ {}}
-@{term inv} & @{term[source]"inv_into UNIV"}
-\end{tabular}
-
-\section{Fixed Points}
-
-Theory: @{theory Inductive}.
-
-Least and greatest fixed points in a complete lattice @{typ 'a}:
-
-\begin{tabular}{@ {} l @ {~::~} l @ {}}
-@{const Inductive.lfp} & @{typeof Inductive.lfp}\\
-@{const Inductive.gfp} & @{typeof Inductive.gfp}\\
-\end{tabular}
-
-Note that in particular sets (@{typ"'a \<Rightarrow> bool"}) are complete lattices.
-
-\section{Sum\_Type}
-
-Type constructor @{text"+"}.
-
-\begin{tabular}{@ {} l @ {~::~} l @ {}}
-@{const Sum_Type.Inl} & @{typeof Sum_Type.Inl}\\
-@{const Sum_Type.Inr} & @{typeof Sum_Type.Inr}\\
-@{const Sum_Type.Plus} & @{term_type_only Sum_Type.Plus "'a set\<Rightarrow>'b set\<Rightarrow>('a+'b)set"}
-\end{tabular}
-
-
-\section{Product\_Type}
-
-Types @{typ unit} and @{text"\<times>"}.
-
-\begin{supertabular}{@ {} l @ {~::~} l @ {}}
-@{const Product_Type.Unity} & @{typeof Product_Type.Unity}\\
-@{const Pair} & @{typeof Pair}\\
-@{const fst} & @{typeof fst}\\
-@{const snd} & @{typeof snd}\\
-@{const split} & @{typeof split}\\
-@{const curry} & @{typeof curry}\\
-@{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} 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 \mbox{@{text"(a, (b, c))"}.}
-Pattern matching with pairs and tuples extends to all binders,
-e.g.\ \mbox{@{prop"ALL (x,y):A. P"},} @{term"{(x,y). P}"}, etc.
-
-
-\section{Relation}
-
-\begin{tabular}{@ {} l @ {~::~} l @ {}}
-@{const Relation.converse} & @{term_type_only Relation.converse "('a * 'b)set \<Rightarrow> ('b*'a)set"}\\
-@{const Relation.relcomp} & @{term_type_only Relation.relcomp "('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.Id} & @{term_type_only Relation.Id "('a*'a)set"}\\
-@{const Relation.Domain} & @{term_type_only Relation.Domain "('a*'b)set\<Rightarrow>'a set"}\\
-@{const Relation.Range} & @{term_type_only Relation.Range "('a*'b)set\<Rightarrow>'b set"}\\
-@{const Relation.Field} & @{term_type_only Relation.Field "('a*'a)set\<Rightarrow>'a set"}\\
-@{const Relation.refl_on} & @{term_type_only Relation.refl_on "'a set\<Rightarrow>('a*'a)set\<Rightarrow>bool"}\\
-@{const Relation.refl} & @{term_type_only Relation.refl "('a*'a)set\<Rightarrow>bool"}\\
-@{const Relation.sym} & @{term_type_only Relation.sym "('a*'a)set\<Rightarrow>bool"}\\
-@{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{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"="} @{expanded_typ "'a rel"}
-
-\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"}\\
-@{const Equiv_Relations.quotient} & @{term_type_only Equiv_Relations.quotient "'a set \<Rightarrow> ('a \<times> 'a) set \<Rightarrow> 'a set set"}\\
-@{const Equiv_Relations.congruent} & @{term_type_only Equiv_Relations.congruent "('a*'a)set\<Rightarrow>('a\<Rightarrow>'b)\<Rightarrow>bool"}\\
-@{const Equiv_Relations.congruent2} & @{term_type_only Equiv_Relations.congruent2 "('a*'a)set\<Rightarrow>('b*'b)set\<Rightarrow>('a\<Rightarrow>'b\<Rightarrow>'c)\<Rightarrow>bool"}\\
-%@ {const Equiv_Relations.} & @ {term_type_only Equiv_Relations. ""}\\
-\end{supertabular}
-
-\subsubsection*{Syntax}
-
-\begin{tabular}{@ {} l @ {\quad$\equiv$\quad} l @ {}}
-@{term"congruent r f"} & @{term[source]"congruent r f"}\\
-@{term"congruent2 r r f"} & @{term[source]"congruent2 r r f"}\\
-\end{tabular}
-
-
-\section{Transitive\_Closure}
-
-\begin{tabular}{@ {} l @ {~::~} l @ {}}
-@{const Transitive_Closure.rtrancl} & @{term_type_only Transitive_Closure.rtrancl "('a*'a)set\<Rightarrow>('a*'a)set"}\\
-@{const Transitive_Closure.trancl} & @{term_type_only Transitive_Closure.trancl "('a*'a)set\<Rightarrow>('a*'a)set"}\\
-@{const Transitive_Closure.reflcl} & @{term_type_only Transitive_Closure.reflcl "('a*'a)set\<Rightarrow>('a*'a)set"}\\
-@{const Transitive_Closure.acyclic} & @{term_type_only Transitive_Closure.acyclic "('a*'a)set\<Rightarrow>bool"}\\
-@{const compower} & @{term_type_only "op ^^ :: ('a*'a)set\<Rightarrow>nat\<Rightarrow>('a*'a)set" "('a*'a)set\<Rightarrow>nat\<Rightarrow>('a*'a)set"}\\
-\end{tabular}
-
-\subsubsection*{Syntax}
-
-\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 Groups}, @{theory Rings}, @{theory Fields} 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}
-
-@{datatype nat}
-\bigskip
-
-\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"} &
-@{term "min :: nat \<Rightarrow> nat \<Rightarrow> nat"} &
-@{term "max :: nat \<Rightarrow> nat \<Rightarrow> nat"} &
-@{term "Min :: nat set \<Rightarrow> nat"} &
-@{term "Max :: nat set \<Rightarrow> nat"}\\
-\end{tabular}
-
-\begin{tabular}{@ {} l @ {~::~} l @ {}}
-@{const Nat.of_nat} & @{typeof Nat.of_nat}\\
-@{term "op ^^ :: ('a \<Rightarrow> 'a) \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> 'a"} &
-  @{term_type_only "op ^^ :: ('a \<Rightarrow> 'a) \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> 'a" "('a \<Rightarrow> 'a) \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> 'a"}
-\end{tabular}
-
-\section{Int}
-
-Type @{typ int}
-\bigskip
-
-\begin{tabular}{@ {} llllllll @ {}}
-@{term "op + :: int \<Rightarrow> int \<Rightarrow> int"} &
-@{term "op - :: int \<Rightarrow> int \<Rightarrow> int"} &
-@{term "uminus :: int \<Rightarrow> int"} &
-@{term "op * :: int \<Rightarrow> int \<Rightarrow> int"} &
-@{term "op ^ :: int \<Rightarrow> nat \<Rightarrow> int"} &
-@{term "op div :: int \<Rightarrow> int \<Rightarrow> int"}&
-@{term "op mod :: int \<Rightarrow> int \<Rightarrow> int"}&
-@{term "op dvd :: int \<Rightarrow> int \<Rightarrow> bool"}\\
-@{term "op \<le> :: int \<Rightarrow> int \<Rightarrow> bool"} &
-@{term "op < :: int \<Rightarrow> int \<Rightarrow> bool"} &
-@{term "min :: int \<Rightarrow> int \<Rightarrow> int"} &
-@{term "max :: int \<Rightarrow> int \<Rightarrow> int"} &
-@{term "Min :: int set \<Rightarrow> int"} &
-@{term "Max :: int set \<Rightarrow> int"}\\
-@{term "abs :: int \<Rightarrow> int"} &
-@{term "sgn :: int \<Rightarrow> int"}\\
-\end{tabular}
-
-\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"} & (\verb$Ints$)
-\end{tabular}
-
-\subsubsection*{Syntax}
-
-\begin{tabular}{@ {} l @ {\quad$\equiv$\quad} l @ {}}
-@{term"of_nat::nat\<Rightarrow>int"} & @{term[source]"of_nat"}\\
-\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 Big_Operators.setsum} & @{term_type_only Big_Operators.setsum "('a => 'b) => 'a set => 'b::comm_monoid_add"}\\
-@{const Big_Operators.setprod} & @{term_type_only Big_Operators.setprod "('a => 'b) => 'a set => 'b::comm_monoid_mult"}\\
-\end{supertabular}
-
-
-\subsubsection*{Syntax}
-
-\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>"}} & (\verb$PROD$)\\
-\end{supertabular}
-
-
-\section{Wellfounded}
-
-\begin{supertabular}{@ {} l @ {~::~} l @ {}}
-@{const Wellfounded.wf} & @{term_type_only Wellfounded.wf "('a*'a)set\<Rightarrow>bool"}\\
-@{const Wellfounded.acc} & @{term_type_only Wellfounded.acc "('a*'a)set\<Rightarrow>'a set"}\\
-@{const Wellfounded.measure} & @{term_type_only Wellfounded.measure "('a\<Rightarrow>nat)\<Rightarrow>('a*'a)set"}\\
-@{const Wellfounded.lex_prod} & @{term_type_only Wellfounded.lex_prod "('a*'a)set\<Rightarrow>('b*'b)set\<Rightarrow>(('a*'b)*('a*'b))set"}\\
-@{const Wellfounded.mlex_prod} & @{term_type_only Wellfounded.mlex_prod "('a\<Rightarrow>nat)\<Rightarrow>('a*'a)set\<Rightarrow>('a*'a)set"}\\
-@{const Wellfounded.less_than} & @{term_type_only Wellfounded.less_than "(nat*nat)set"}\\
-@{const Wellfounded.pred_nat} & @{term_type_only Wellfounded.pred_nat "(nat*nat)set"}\\
-\end{supertabular}
-
-
-\section{SetInterval}
-
-\begin{supertabular}{@ {} l @ {~::~} l @ {}}
-@{const lessThan} & @{term_type_only lessThan "'a::ord \<Rightarrow> 'a set"}\\
-@{const atMost} & @{term_type_only atMost "'a::ord \<Rightarrow> 'a set"}\\
-@{const greaterThan} & @{term_type_only greaterThan "'a::ord \<Rightarrow> 'a set"}\\
-@{const atLeast} & @{term_type_only atLeast "'a::ord \<Rightarrow> 'a set"}\\
-@{const greaterThanLessThan} & @{term_type_only greaterThanLessThan "'a::ord \<Rightarrow> 'a \<Rightarrow> 'a set"}\\
-@{const atLeastLessThan} & @{term_type_only atLeastLessThan "'a::ord \<Rightarrow> 'a \<Rightarrow> 'a set"}\\
-@{const greaterThanAtMost} & @{term_type_only greaterThanAtMost "'a::ord \<Rightarrow> 'a \<Rightarrow> 'a set"}\\
-@{const atLeastAtMost} & @{term_type_only atLeastAtMost "'a::ord \<Rightarrow> 'a \<Rightarrow> 'a set"}\\
-\end{supertabular}
-
-\subsubsection*{Syntax}
-
-\begin{supertabular}{@ {} l @ {\quad$\equiv$\quad} l @ {}}
-@{term "lessThan y"} & @{term[source] "lessThan y"}\\
-@{term "atMost y"} & @{term[source] "atMost y"}\\
-@{term "greaterThan x"} & @{term[source] "greaterThan x"}\\
-@{term "atLeast x"} & @{term[source] "atLeast x"}\\
-@{term "greaterThanLessThan x y"} & @{term[source] "greaterThanLessThan x y"}\\
-@{term "atLeastLessThan x y"} & @{term[source] "atLeastLessThan x y"}\\
-@{term "greaterThanAtMost x y"} & @{term[source] "greaterThanAtMost x y"}\\
-@{term "atLeastAtMost x y"} & @{term[source] "atLeastAtMost x y"}\\
-@{term[mode=xsymbols] "UN i:{..n}. A"} & @{term[source] "\<Union> i \<in> {..n}. A"}\\
-@{term[mode=xsymbols] "UN i:{..<n}. A"} & @{term[source] "\<Union> i \<in> {..<n}. A"}\\
-\multicolumn{2}{@ {}l@ {}}{Similarly for @{text"\<Inter>"} instead of @{text"\<Union>"}}\\
-@{term "setsum (%x. t) {a..b}"} & @{term[source] "setsum (\<lambda>x. t) {a..b}"}\\
-@{term "setsum (%x. t) {a..<b}"} & @{term[source] "setsum (\<lambda>x. t) {a..<b}"}\\
-@{term "setsum (%x. t) {..b}"} & @{term[source] "setsum (\<lambda>x. t) {..b}"}\\
-@{term "setsum (%x. t) {..<b}"} & @{term[source] "setsum (\<lambda>x. t) {..<b}"}\\
-\multicolumn{2}{@ {}l@ {}}{Similarly for @{text"\<Prod>"} instead of @{text"\<Sum>"}}\\
-\end{supertabular}
-
-
-\section{Power}
-
-\begin{tabular}{@ {} l @ {~::~} l @ {}}
-@{const Power.power} & @{typeof Power.power}
-\end{tabular}
-
-
-\section{Option}
-
-@{datatype option}
-\bigskip
-
-\begin{tabular}{@ {} l @ {~::~} l @ {}}
-@{const Option.the} & @{typeof Option.the}\\
-@{const Option.map} & @{typ[source]"('a \<Rightarrow> 'b) \<Rightarrow> 'a option \<Rightarrow> 'b option"}\\
-@{const Option.set} & @{term_type_only Option.set "'a option \<Rightarrow> 'a set"}\\
-@{const Option.bind} & @{term_type_only Option.bind "'a option \<Rightarrow> ('a \<Rightarrow> 'b option) \<Rightarrow> 'b option"}
-\end{tabular}
-
-\section{List}
-
-@{datatype list}
-\bigskip
-
-\begin{supertabular}{@ {} l @ {~::~} l @ {}}
-@{const List.append} & @{typeof List.append}\\
-@{const List.butlast} & @{typeof List.butlast}\\
-@{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}\\
-@{const List.length} & @{typeof List.length}\\
-@{const List.lenlex} & @{term_type_only List.lenlex "('a*'a)set\<Rightarrow>('a list * 'a list)set"}\\
-@{const List.lex} & @{term_type_only List.lex "('a*'a)set\<Rightarrow>('a list * 'a list)set"}\\
-@{const List.lexn} & @{term_type_only List.lexn "('a*'a)set\<Rightarrow>nat\<Rightarrow>('a list * 'a list)set"}\\
-@{const List.lexord} & @{term_type_only List.lexord "('a*'a)set\<Rightarrow>('a list * 'a list)set"}\\
-@{const List.listrel} & @{term_type_only List.listrel "('a*'b)set\<Rightarrow>('a list * 'b list)set"}\\
-@{const List.listrel1} & @{term_type_only List.listrel1 "('a*'a)set\<Rightarrow>('a list * 'a list)set"}\\
-@{const List.lists} & @{term_type_only List.lists "'a set\<Rightarrow>'a list set"}\\
-@{const List.listset} & @{term_type_only List.listset "'a set list \<Rightarrow> 'a list set"}\\
-@{const List.listsum} & @{typeof List.listsum}\\
-@{const List.list_all2} & @{typeof List.list_all2}\\
-@{const List.list_update} & @{typeof List.list_update}\\
-@{const List.map} & @{typeof List.map}\\
-@{const List.measures} & @{term_type_only List.measures "('a\<Rightarrow>nat)list\<Rightarrow>('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}\\
-@{const List.replicate} & @{typeof List.replicate}\\
-@{const List.rev} & @{typeof List.rev}\\
-@{const List.rotate} & @{typeof List.rotate}\\
-@{const List.rotate1} & @{typeof List.rotate1}\\
-@{const List.set} & @{term_type_only List.set "'a list \<Rightarrow> 'a set"}\\
-@{const List.sort} & @{typeof List.sort}\\
-@{const List.sorted} & @{typeof List.sorted}\\
-@{const List.splice} & @{typeof List.splice}\\
-@{const List.sublist} & @{typeof List.sublist}\\
-@{const List.take} & @{typeof List.take}\\
-@{const List.takeWhile} & @{typeof List.takeWhile}\\
-@{const List.tl} & @{typeof List.tl}\\
-@{const List.upt} & @{typeof List.upt}\\
-@{const List.upto} & @{typeof List.upto}\\
-@{const List.zip} & @{typeof List.zip}\\
-\end{supertabular}
-
-\subsubsection*{Syntax}
-
-\begin{supertabular}{@ {} l @ {\quad$\equiv$\quad} l @ {}}
-@{text"[x\<^isub>1,\<dots>,x\<^isub>n]"} & @{text"x\<^isub>1 # \<dots> # x\<^isub>n # []"}\\
-@{term"[m..<n]"} & @{term[source]"upt m n"}\\
-@{term"[i..j]"} & @{term[source]"upto i j"}\\
-@{text"[e. x \<leftarrow> xs]"} & @{term"map (%x. e) xs"}\\
-@{term"[x \<leftarrow> xs. b]"} & @{term[source]"filter (\<lambda>x. b) xs"} \\
-@{term"xs[n := x]"} & @{term[source]"list_update xs n x"}\\
-@{term"\<Sum>x\<leftarrow>xs. e"} & @{term[source]"listsum (map (\<lambda>x. e) xs)"}\\
-\end{supertabular}
-\medskip
-
-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}
-
-Maps model partial functions and are often used as finite tables. However,
-the domain of a map may be infinite.
-
-\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)"}\\
-@{const Map.dom} & @{term_type_only Map.dom "('a\<Rightarrow>'b option)\<Rightarrow>'a set"}\\
-@{const Map.ran} & @{term_type_only Map.ran "('a\<Rightarrow>'b option)\<Rightarrow>'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{supertabular}
-
-\subsubsection*{Syntax}
-
-\begin{tabular}{@ {} l @ {\quad$\equiv$\quad} l @ {}}
-@{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}
-
-*}
-(*<*)
-end
-(*>*)
\ No newline at end of file

--- a/doc-src/Main/Docs/document/Main_Doc.tex	Mon Aug 27 21:19:16 2012 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,613 +0,0 @@
-%
-\begin{isabellebody}%
-\def\isabellecontext{Main{\isaliteral{5F}{\isacharunderscore}}Doc}%
-%
-\isadelimtheory
-%
-\endisadelimtheory
-%
-\isatagtheory
-%
-\endisatagtheory
-{\isafoldtheory}%
-%
-\isadelimtheory
-%
-\endisadelimtheory
-%
-\isadelimML
-%
-\endisadelimML
-%
-\isatagML
-%
-\endisatagML
-{\isafoldML}%
-%
-\isadelimML
-%
-\endisadelimML
-%
-\begin{isamarkuptext}%
-\begin{abstract}
-This document lists the main types, functions and syntax provided by theory \isa{Main}. It is meant as a quick overview of what is available. The sophisticated class structure is only hinted at. For details see \url{http://isabelle.in.tum.de/library/HOL/}.
-\end{abstract}
-
-\section{HOL}
-
-The basic logic: \isa{x\ {\isaliteral{3D}{\isacharequal}}\ y}, \isa{True}, \isa{False}, \isa{{\isaliteral{5C3C6E6F743E}{\isasymnot}}\ P}, \isa{P\ {\isaliteral{5C3C616E643E}{\isasymand}}\ Q}, \isa{P\ {\isaliteral{5C3C6F723E}{\isasymor}}\ Q}, \isa{P\ {\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}\ Q}, \isa{{\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}x{\isaliteral{2E}{\isachardot}}\ P}, \isa{{\isaliteral{5C3C6578697374733E}{\isasymexists}}x{\isaliteral{2E}{\isachardot}}\ P}, \isa{{\isaliteral{5C3C6578697374733E}{\isasymexists}}{\isaliteral{21}{\isacharbang}}x{\isaliteral{2E}{\isachardot}}\ P}, \isa{THE\ x{\isaliteral{2E}{\isachardot}}\ P}.
-\smallskip
-
-\begin{tabular}{@ {} l @ {~::~} l @ {}}
-\isa{undefined} & \isa{{\isaliteral{27}{\isacharprime}}a}\\
-\isa{default} & \isa{{\isaliteral{27}{\isacharprime}}a}\\
-\end{tabular}
-
-\subsubsection*{Syntax}
-
-\begin{supertabular}{@ {} l @ {\quad$\equiv$\quad} l l @ {}}
-\isa{x\ {\isaliteral{5C3C6E6F7465713E}{\isasymnoteq}}\ y} & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C6E6F743E}{\isasymnot}}\ {\isaliteral{28}{\isacharparenleft}}x\ {\isaliteral{3D}{\isacharequal}}\ y{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} & (\verb$~=$)\\
-\isa{{\isaliteral{22}{\isachardoublequote}}P\ {\isaliteral{5C3C6C6F6E676C65667472696768746172726F773E}{\isasymlongleftrightarrow}}\ Q{\isaliteral{22}{\isachardoublequote}}} & \isa{P\ {\isaliteral{3D}{\isacharequal}}\ Q} \\
-\isa{if\ x\ then\ y\ else\ z} & \isa{{\isaliteral{22}{\isachardoublequote}}If\ x\ y\ z{\isaliteral{22}{\isachardoublequote}}}\\
-\isa{let\ x\ {\isaliteral{3D}{\isacharequal}}\ e\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}\ in\ e\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{2}}} & \isa{{\isaliteral{22}{\isachardoublequote}}Let\ e\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6C616D6264613E}{\isasymlambda}}x{\isaliteral{2E}{\isachardot}}\ e\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{2}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}}\\
-\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 @ {}}
-\isa{op\ {\isaliteral{5C3C6C653E}{\isasymle}}} & \isa{{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ bool} & (\verb$<=$)\\
-\isa{op\ {\isaliteral{3C}{\isacharless}}} & \isa{{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ bool}\\
-\isa{Least} & \isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ bool{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a}\\
-\isa{min} & \isa{{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a}\\
-\isa{max} & \isa{{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a}\\
-\isa{top} & \isa{{\isaliteral{27}{\isacharprime}}a}\\
-\isa{bot} & \isa{{\isaliteral{27}{\isacharprime}}a}\\
-\isa{mono} & \isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}b{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ bool}\\
-\isa{strict{\isaliteral{5F}{\isacharunderscore}}mono} & \isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}b{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ bool}\\
-\end{supertabular}
-
-\subsubsection*{Syntax}
-
-\begin{supertabular}{@ {} l @ {\quad$\equiv$\quad} l l @ {}}
-\isa{{\isaliteral{22}{\isachardoublequote}}x\ {\isaliteral{5C3C67653E}{\isasymge}}\ y{\isaliteral{22}{\isachardoublequote}}} & \isa{y\ {\isaliteral{5C3C6C653E}{\isasymle}}\ x} & (\verb$>=$)\\
-\isa{{\isaliteral{22}{\isachardoublequote}}x\ {\isaliteral{3E}{\isachargreater}}\ y{\isaliteral{22}{\isachardoublequote}}} & \isa{y\ {\isaliteral{3C}{\isacharless}}\ x}\\
-\isa{{\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}x{\isaliteral{5C3C6C653E}{\isasymle}}y{\isaliteral{2E}{\isachardot}}\ P} & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}x{\isaliteral{2E}{\isachardot}}\ x\ {\isaliteral{5C3C6C653E}{\isasymle}}\ y\ {\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}\ P{\isaliteral{22}{\isachardoublequote}}}\\
-\isa{{\isaliteral{5C3C6578697374733E}{\isasymexists}}x{\isaliteral{5C3C6C653E}{\isasymle}}y{\isaliteral{2E}{\isachardot}}\ P} & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C6578697374733E}{\isasymexists}}x{\isaliteral{2E}{\isachardot}}\ x\ {\isaliteral{5C3C6C653E}{\isasymle}}\ y\ {\isaliteral{5C3C616E643E}{\isasymand}}\ P{\isaliteral{22}{\isachardoublequote}}}\\
-\multicolumn{2}{@ {}l@ {}}{Similarly for $<$, $\ge$ and $>$}\\
-\isa{LEAST\ x{\isaliteral{2E}{\isachardot}}\ P} & \isa{{\isaliteral{22}{\isachardoublequote}}Least\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6C616D6264613E}{\isasymlambda}}x{\isaliteral{2E}{\isachardot}}\ P{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}}\\
-\end{supertabular}
-
-
-\section{Lattices}
-
-Classes semilattice, lattice, distributive lattice and complete lattice (the
-latter in theory \isa{Set}).
-
-\begin{tabular}{@ {} l @ {~::~} l @ {}}
-\isa{inf} & \isa{{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a}\\
-\isa{sup} & \isa{{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a}\\
-\isa{Inf} & \isa{{\isaliteral{27}{\isacharprime}}a\ set\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a}\\
-\isa{Sup} & \isa{{\isaliteral{27}{\isacharprime}}a\ set\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a}\\
-\end{tabular}
-
-\subsubsection*{Syntax}
-
-Available by loading theory \isa{Lattice{\isaliteral{5F}{\isacharunderscore}}Syntax} in directory \isa{Library}.
-
-\begin{supertabular}{@ {} l @ {\quad$\equiv$\quad} l @ {}}
-\isa{{\isaliteral{22}{\isachardoublequote}}x\ {\isaliteral{5C3C737173756273657465713E}{\isasymsqsubseteq}}\ y{\isaliteral{22}{\isachardoublequote}}} & \isa{x\ {\isaliteral{5C3C6C653E}{\isasymle}}\ y}\\
-\isa{{\isaliteral{22}{\isachardoublequote}}x\ {\isaliteral{5C3C73717375627365743E}{\isasymsqsubset}}\ y{\isaliteral{22}{\isachardoublequote}}} & \isa{x\ {\isaliteral{3C}{\isacharless}}\ y}\\
-\isa{{\isaliteral{22}{\isachardoublequote}}x\ {\isaliteral{5C3C7371696E7465723E}{\isasymsqinter}}\ y{\isaliteral{22}{\isachardoublequote}}} & \isa{inf\ x\ y}\\
-\isa{{\isaliteral{22}{\isachardoublequote}}x\ {\isaliteral{5C3C7371756E696F6E3E}{\isasymsqunion}}\ y{\isaliteral{22}{\isachardoublequote}}} & \isa{sup\ x\ y}\\
-\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C5371696E7465723E}{\isasymSqinter}}\ A{\isaliteral{22}{\isachardoublequote}}} & \isa{Sup\ A}\\
-\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C5371756E696F6E3E}{\isasymSqunion}}\ A{\isaliteral{22}{\isachardoublequote}}} & \isa{Inf\ A}\\
-\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C746F703E}{\isasymtop}}{\isaliteral{22}{\isachardoublequote}}} & \isa{top}\\
-\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C626F74746F6D3E}{\isasymbottom}}{\isaliteral{22}{\isachardoublequote}}} & \isa{bot}\\
-\end{supertabular}
-
-
-\section{Set}
-
-%Sets are predicates: \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{27}{\isacharprime}}a\ set\ \ {\isaliteral{3D}{\isacharequal}}\ \ {\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ bool{\isaliteral{22}{\isachardoublequote}}}
-%\bigskip
-
-\begin{supertabular}{@ {} l @ {~::~} l l @ {}}
-\isa{{\isaliteral{7B}{\isacharbraceleft}}{\isaliteral{7D}{\isacharbraceright}}} & \isa{{\isaliteral{27}{\isacharprime}}a\ set}\\
-\isa{insert} & \isa{{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ set\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ set}\\
-\isa{Collect} & \isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ bool{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ set}\\
-\isa{op\ {\isaliteral{5C3C696E3E}{\isasymin}}} & \isa{{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ set\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ bool} & (\texttt{:})\\
-\isa{op\ {\isaliteral{5C3C756E696F6E3E}{\isasymunion}}} & \isa{{\isaliteral{27}{\isacharprime}}a\ set\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ set\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ set} & (\texttt{Un})\\
-\isa{op\ {\isaliteral{5C3C696E7465723E}{\isasyminter}}} & \isa{{\isaliteral{27}{\isacharprime}}a\ set\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ set\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ set} & (\texttt{Int})\\
-\isa{UNION} & \isa{{\isaliteral{27}{\isacharprime}}a\ set\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}b\ set{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}b\ set}\\
-\isa{INTER} & \isa{{\isaliteral{27}{\isacharprime}}a\ set\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}b\ set{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}b\ set}\\
-\isa{Union} & \isa{{\isaliteral{27}{\isacharprime}}a\ set\ set\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ set}\\
-\isa{Inter} & \isa{{\isaliteral{27}{\isacharprime}}a\ set\ set\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ set}\\
-\isa{Pow} & \isa{{\isaliteral{27}{\isacharprime}}a\ set\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ set\ set}\\
-\isa{UNIV} & \isa{{\isaliteral{27}{\isacharprime}}a\ set}\\
-\isa{op\ {\isaliteral{60}{\isacharbackquote}}} & \isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}b{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ set\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}b\ set}\\
-\isa{Ball} & \isa{{\isaliteral{27}{\isacharprime}}a\ set\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ bool{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ bool}\\
-\isa{Bex} & \isa{{\isaliteral{27}{\isacharprime}}a\ set\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ bool{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ bool}\\
-\end{supertabular}
-
-\subsubsection*{Syntax}
-
-\begin{supertabular}{@ {} l @ {\quad$\equiv$\quad} l l @ {}}
-\isa{{\isaliteral{7B}{\isacharbraceleft}}x\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}x\isaliteral{5C3C5E697375623E}{}\isactrlisub n{\isaliteral{7D}{\isacharbraceright}}} & \isa{insert\ x\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C646F74733E}{\isasymdots}}\ {\isaliteral{28}{\isacharparenleft}}insert\ x\isaliteral{5C3C5E697375623E}{}\isactrlisub n\ {\isaliteral{7B}{\isacharbraceleft}}{\isaliteral{7D}{\isacharbraceright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{29}{\isacharparenright}}}\\
-\isa{x\ {\isaliteral{5C3C6E6F74696E3E}{\isasymnotin}}\ A} & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C6E6F743E}{\isasymnot}}{\isaliteral{28}{\isacharparenleft}}x\ {\isaliteral{5C3C696E3E}{\isasymin}}\ A{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}}\\
-\isa{A\ {\isaliteral{5C3C73756273657465713E}{\isasymsubseteq}}\ B} & \isa{{\isaliteral{22}{\isachardoublequote}}A\ {\isaliteral{5C3C6C653E}{\isasymle}}\ B{\isaliteral{22}{\isachardoublequote}}}\\
-\isa{A\ {\isaliteral{5C3C7375627365743E}{\isasymsubset}}\ B} & \isa{{\isaliteral{22}{\isachardoublequote}}A\ {\isaliteral{3C}{\isacharless}}\ B{\isaliteral{22}{\isachardoublequote}}}\\
-\isa{{\isaliteral{22}{\isachardoublequote}}A\ {\isaliteral{5C3C73757073657465713E}{\isasymsupseteq}}\ B{\isaliteral{22}{\isachardoublequote}}} & \isa{{\isaliteral{22}{\isachardoublequote}}B\ {\isaliteral{5C3C6C653E}{\isasymle}}\ A{\isaliteral{22}{\isachardoublequote}}}\\
-\isa{{\isaliteral{22}{\isachardoublequote}}A\ {\isaliteral{5C3C7375707365743E}{\isasymsupset}}\ B{\isaliteral{22}{\isachardoublequote}}} & \isa{{\isaliteral{22}{\isachardoublequote}}B\ {\isaliteral{3C}{\isacharless}}\ A{\isaliteral{22}{\isachardoublequote}}}\\
-\isa{{\isaliteral{7B}{\isacharbraceleft}}x{\isaliteral{2E}{\isachardot}}\ P{\isaliteral{7D}{\isacharbraceright}}} & \isa{{\isaliteral{22}{\isachardoublequote}}Collect\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6C616D6264613E}{\isasymlambda}}x{\isaliteral{2E}{\isachardot}}\ P{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}}\\
-\isa{{\isaliteral{5C3C556E696F6E3E}{\isasymUnion}}x{\isaliteral{5C3C696E3E}{\isasymin}}I{\isaliteral{2E}{\isachardot}}\ A} & \isa{{\isaliteral{22}{\isachardoublequote}}UNION\ I\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6C616D6264613E}{\isasymlambda}}x{\isaliteral{2E}{\isachardot}}\ A{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} & (\texttt{UN})\\
-\isa{{\isaliteral{5C3C556E696F6E3E}{\isasymUnion}}x{\isaliteral{2E}{\isachardot}}\ A} & \isa{{\isaliteral{22}{\isachardoublequote}}UNION\ UNIV\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6C616D6264613E}{\isasymlambda}}x{\isaliteral{2E}{\isachardot}}\ A{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}}\\
-\isa{{\isaliteral{5C3C496E7465723E}{\isasymInter}}x{\isaliteral{5C3C696E3E}{\isasymin}}I{\isaliteral{2E}{\isachardot}}\ A} & \isa{{\isaliteral{22}{\isachardoublequote}}INTER\ I\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6C616D6264613E}{\isasymlambda}}x{\isaliteral{2E}{\isachardot}}\ A{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} & (\texttt{INT})\\
-\isa{{\isaliteral{5C3C496E7465723E}{\isasymInter}}x{\isaliteral{2E}{\isachardot}}\ A} & \isa{{\isaliteral{22}{\isachardoublequote}}INTER\ UNIV\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6C616D6264613E}{\isasymlambda}}x{\isaliteral{2E}{\isachardot}}\ A{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}}\\
-\isa{{\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}x{\isaliteral{5C3C696E3E}{\isasymin}}A{\isaliteral{2E}{\isachardot}}\ P} & \isa{{\isaliteral{22}{\isachardoublequote}}Ball\ A\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6C616D6264613E}{\isasymlambda}}x{\isaliteral{2E}{\isachardot}}\ P{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}}\\
-\isa{{\isaliteral{5C3C6578697374733E}{\isasymexists}}x{\isaliteral{5C3C696E3E}{\isasymin}}A{\isaliteral{2E}{\isachardot}}\ P} & \isa{{\isaliteral{22}{\isachardoublequote}}Bex\ A\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6C616D6264613E}{\isasymlambda}}x{\isaliteral{2E}{\isachardot}}\ P{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}}\\
-\isa{range\ f} & \isa{{\isaliteral{22}{\isachardoublequote}}f\ {\isaliteral{60}{\isacharbackquote}}\ UNIV{\isaliteral{22}{\isachardoublequote}}}\\
-\end{supertabular}
-
-
-\section{Fun}
-
-\begin{supertabular}{@ {} l @ {~::~} l l @ {}}
-\isa{id} & \isa{{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a}\\
-\isa{op\ {\isaliteral{5C3C636972633E}{\isasymcirc}}} & \isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}b{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}c\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}c\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}b} & (\texttt{o})\\
-\isa{inj{\isaliteral{5F}{\isacharunderscore}}on} & \isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}b{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ set\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ bool}\\
-\isa{inj} & \isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}b{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ bool}\\
-\isa{surj} & \isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}b{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ bool}\\
-\isa{bij} & \isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}b{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ bool}\\
-\isa{bij{\isaliteral{5F}{\isacharunderscore}}betw} & \isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}b{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ set\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}b\ set\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ bool}\\
-\isa{fun{\isaliteral{5F}{\isacharunderscore}}upd} & \isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}b{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}b\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}b}\\
-\end{supertabular}
-
-\subsubsection*{Syntax}
-
-\begin{tabular}{@ {} l @ {\quad$\equiv$\quad} l @ {}}
-\isa{f{\isaliteral{28}{\isacharparenleft}}x\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3D}{\isacharequal}}\ y{\isaliteral{29}{\isacharparenright}}} & \isa{{\isaliteral{22}{\isachardoublequote}}fun{\isaliteral{5F}{\isacharunderscore}}upd\ f\ x\ y{\isaliteral{22}{\isachardoublequote}}}\\
-\isa{f{\isaliteral{28}{\isacharparenleft}}x\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3D}{\isacharequal}}y\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}x\isaliteral{5C3C5E697375623E}{}\isactrlisub n{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3D}{\isacharequal}}y\isaliteral{5C3C5E697375623E}{}\isactrlisub n{\isaliteral{29}{\isacharparenright}}} & \isa{f{\isaliteral{28}{\isacharparenleft}}x\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3D}{\isacharequal}}y\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{28}{\isacharparenleft}}x\isaliteral{5C3C5E697375623E}{}\isactrlisub n{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3D}{\isacharequal}}y\isaliteral{5C3C5E697375623E}{}\isactrlisub n{\isaliteral{29}{\isacharparenright}}}\\
-\end{tabular}
-
-
-\section{Hilbert\_Choice}
-
-Hilbert's selection ($\varepsilon$) operator: \isa{SOME\ x{\isaliteral{2E}{\isachardot}}\ P}.
-\smallskip
-
-\begin{tabular}{@ {} l @ {~::~} l @ {}}
-\isa{inv{\isaliteral{5F}{\isacharunderscore}}into} & \isa{{\isaliteral{27}{\isacharprime}}a\ set\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}b{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}b\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a}
-\end{tabular}
-
-\subsubsection*{Syntax}
-
-\begin{tabular}{@ {} l @ {\quad$\equiv$\quad} l @ {}}
-\isa{inv} & \isa{{\isaliteral{22}{\isachardoublequote}}inv{\isaliteral{5F}{\isacharunderscore}}into\ UNIV{\isaliteral{22}{\isachardoublequote}}}
-\end{tabular}
-
-\section{Fixed Points}
-
-Theory: \isa{Inductive}.
-
-Least and greatest fixed points in a complete lattice \isa{{\isaliteral{27}{\isacharprime}}a}:
-
-\begin{tabular}{@ {} l @ {~::~} l @ {}}
-\isa{lfp} & \isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a}\\
-\isa{gfp} & \isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a}\\
-\end{tabular}
-
-Note that in particular sets (\isa{{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ bool}) are complete lattices.
-
-\section{Sum\_Type}
-
-Type constructor \isa{{\isaliteral{2B}{\isacharplus}}}.
-
-\begin{tabular}{@ {} l @ {~::~} l @ {}}
-\isa{Inl} & \isa{{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ {\isaliteral{2B}{\isacharplus}}\ {\isaliteral{27}{\isacharprime}}b}\\
-\isa{Inr} & \isa{{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}b\ {\isaliteral{2B}{\isacharplus}}\ {\isaliteral{27}{\isacharprime}}a}\\
-\isa{op\ {\isaliteral{3C}{\isacharless}}{\isaliteral{2B}{\isacharplus}}{\isaliteral{3E}{\isachargreater}}} & \isa{{\isaliteral{27}{\isacharprime}}a\ set\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}b\ set\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{2B}{\isacharplus}}\ {\isaliteral{27}{\isacharprime}}b{\isaliteral{29}{\isacharparenright}}\ set}
-\end{tabular}
-
-
-\section{Product\_Type}
-
-Types \isa{unit} and \isa{{\isaliteral{5C3C74696D65733E}{\isasymtimes}}}.
-
-\begin{supertabular}{@ {} l @ {~::~} l @ {}}
-\isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{29}{\isacharparenright}}} & \isa{unit}\\
-\isa{Pair} & \isa{{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}b\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C74696D65733E}{\isasymtimes}}\ {\isaliteral{27}{\isacharprime}}b}\\
-\isa{fst} & \isa{{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C74696D65733E}{\isasymtimes}}\ {\isaliteral{27}{\isacharprime}}b\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a}\\
-\isa{snd} & \isa{{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C74696D65733E}{\isasymtimes}}\ {\isaliteral{27}{\isacharprime}}b\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}b}\\
-\isa{split} & \isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}b\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}c{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C74696D65733E}{\isasymtimes}}\ {\isaliteral{27}{\isacharprime}}b\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}c}\\
-\isa{curry} & \isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C74696D65733E}{\isasymtimes}}\ {\isaliteral{27}{\isacharprime}}b\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}c{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}b\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}c}\\
-\isa{Sigma} & \isa{{\isaliteral{27}{\isacharprime}}a\ set\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}b\ set{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C74696D65733E}{\isasymtimes}}\ {\isaliteral{27}{\isacharprime}}b{\isaliteral{29}{\isacharparenright}}\ set}\\
-\end{supertabular}
-
-\subsubsection*{Syntax}
-
-\begin{tabular}{@ {} l @ {\quad$\equiv$\quad} ll @ {}}
-\isa{{\isaliteral{28}{\isacharparenleft}}a{\isaliteral{2C}{\isacharcomma}}\ b{\isaliteral{29}{\isacharparenright}}} & \isa{{\isaliteral{22}{\isachardoublequote}}Pair\ a\ b{\isaliteral{22}{\isachardoublequote}}}\\
-\isa{{\isaliteral{5C3C6C616D6264613E}{\isasymlambda}}{\isaliteral{28}{\isacharparenleft}}x{\isaliteral{2C}{\isacharcomma}}\ y{\isaliteral{29}{\isacharparenright}}{\isaliteral{2E}{\isachardot}}\ t} & \isa{{\isaliteral{22}{\isachardoublequote}}split\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6C616D6264613E}{\isasymlambda}}x\ y{\isaliteral{2E}{\isachardot}}\ t{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}}\\
-\isa{A\ {\isaliteral{5C3C74696D65733E}{\isasymtimes}}\ B} &  \isa{Sigma\ A\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6C616D6264613E}{\isasymlambda}}\_{\isaliteral{2E}{\isachardot}}\ B{\isaliteral{29}{\isacharparenright}}} & (\verb$<*>$)
-\end{tabular}
-
-Pairs may be nested. Nesting to the right is printed as a tuple,
-e.g.\ \mbox{\isa{{\isaliteral{28}{\isacharparenleft}}a{\isaliteral{2C}{\isacharcomma}}\ b{\isaliteral{2C}{\isacharcomma}}\ c{\isaliteral{29}{\isacharparenright}}}} is really \mbox{\isa{{\isaliteral{28}{\isacharparenleft}}a{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{28}{\isacharparenleft}}b{\isaliteral{2C}{\isacharcomma}}\ c{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}}.}
-Pattern matching with pairs and tuples extends to all binders,
-e.g.\ \mbox{\isa{{\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}{\isaliteral{28}{\isacharparenleft}}x{\isaliteral{2C}{\isacharcomma}}\ y{\isaliteral{29}{\isacharparenright}}{\isaliteral{5C3C696E3E}{\isasymin}}A{\isaliteral{2E}{\isachardot}}\ P},} \isa{{\isaliteral{7B}{\isacharbraceleft}}{\isaliteral{28}{\isacharparenleft}}x{\isaliteral{2C}{\isacharcomma}}\ y{\isaliteral{29}{\isacharparenright}}{\isaliteral{2E}{\isachardot}}\ P{\isaliteral{7D}{\isacharbraceright}}}, etc.
-
-
-\section{Relation}
-
-\begin{tabular}{@ {} l @ {~::~} l @ {}}
-\isa{converse} & \isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C74696D65733E}{\isasymtimes}}\ {\isaliteral{27}{\isacharprime}}b{\isaliteral{29}{\isacharparenright}}\ set\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}b\ {\isaliteral{5C3C74696D65733E}{\isasymtimes}}\ {\isaliteral{27}{\isacharprime}}a{\isaliteral{29}{\isacharparenright}}\ set}\\
-\isa{op\ O} & \isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C74696D65733E}{\isasymtimes}}\ {\isaliteral{27}{\isacharprime}}b{\isaliteral{29}{\isacharparenright}}\ set\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}b\ {\isaliteral{5C3C74696D65733E}{\isasymtimes}}\ {\isaliteral{27}{\isacharprime}}c{\isaliteral{29}{\isacharparenright}}\ set\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C74696D65733E}{\isasymtimes}}\ {\isaliteral{27}{\isacharprime}}c{\isaliteral{29}{\isacharparenright}}\ set}\\
-\isa{op\ {\isaliteral{60}{\isacharbackquote}}{\isaliteral{60}{\isacharbackquote}}} & \isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C74696D65733E}{\isasymtimes}}\ {\isaliteral{27}{\isacharprime}}b{\isaliteral{29}{\isacharparenright}}\ set\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ set\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}b\ set}\\
-\isa{inv{\isaliteral{5F}{\isacharunderscore}}image} & \isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C74696D65733E}{\isasymtimes}}\ {\isaliteral{27}{\isacharprime}}a{\isaliteral{29}{\isacharparenright}}\ set\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}b\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}b\ {\isaliteral{5C3C74696D65733E}{\isasymtimes}}\ {\isaliteral{27}{\isacharprime}}b{\isaliteral{29}{\isacharparenright}}\ set}\\
-\isa{Id{\isaliteral{5F}{\isacharunderscore}}on} & \isa{{\isaliteral{27}{\isacharprime}}a\ set\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C74696D65733E}{\isasymtimes}}\ {\isaliteral{27}{\isacharprime}}a{\isaliteral{29}{\isacharparenright}}\ set}\\
-\isa{Id} & \isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C74696D65733E}{\isasymtimes}}\ {\isaliteral{27}{\isacharprime}}a{\isaliteral{29}{\isacharparenright}}\ set}\\
-\isa{Domain} & \isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C74696D65733E}{\isasymtimes}}\ {\isaliteral{27}{\isacharprime}}b{\isaliteral{29}{\isacharparenright}}\ set\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ set}\\
-\isa{Range} & \isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C74696D65733E}{\isasymtimes}}\ {\isaliteral{27}{\isacharprime}}b{\isaliteral{29}{\isacharparenright}}\ set\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}b\ set}\\
-\isa{Field} & \isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C74696D65733E}{\isasymtimes}}\ {\isaliteral{27}{\isacharprime}}a{\isaliteral{29}{\isacharparenright}}\ set\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ set}\\
-\isa{refl{\isaliteral{5F}{\isacharunderscore}}on} & \isa{{\isaliteral{27}{\isacharprime}}a\ set\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C74696D65733E}{\isasymtimes}}\ {\isaliteral{27}{\isacharprime}}a{\isaliteral{29}{\isacharparenright}}\ set\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ bool}\\
-\isa{refl} & \isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C74696D65733E}{\isasymtimes}}\ {\isaliteral{27}{\isacharprime}}a{\isaliteral{29}{\isacharparenright}}\ set\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ bool}\\
-\isa{sym} & \isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C74696D65733E}{\isasymtimes}}\ {\isaliteral{27}{\isacharprime}}a{\isaliteral{29}{\isacharparenright}}\ set\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ bool}\\
-\isa{antisym} & \isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C74696D65733E}{\isasymtimes}}\ {\isaliteral{27}{\isacharprime}}a{\isaliteral{29}{\isacharparenright}}\ set\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ bool}\\
-\isa{trans} & \isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C74696D65733E}{\isasymtimes}}\ {\isaliteral{27}{\isacharprime}}a{\isaliteral{29}{\isacharparenright}}\ set\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ bool}\\
-\isa{irrefl} & \isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C74696D65733E}{\isasymtimes}}\ {\isaliteral{27}{\isacharprime}}a{\isaliteral{29}{\isacharparenright}}\ set\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ bool}\\
-\isa{total{\isaliteral{5F}{\isacharunderscore}}on} & \isa{{\isaliteral{27}{\isacharprime}}a\ set\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C74696D65733E}{\isasymtimes}}\ {\isaliteral{27}{\isacharprime}}a{\isaliteral{29}{\isacharparenright}}\ set\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ bool}\\
-\isa{total} & \isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C74696D65733E}{\isasymtimes}}\ {\isaliteral{27}{\isacharprime}}a{\isaliteral{29}{\isacharparenright}}\ set\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ bool}\\
-\end{tabular}
-
-\subsubsection*{Syntax}
-
-\begin{tabular}{@ {} l @ {\quad$\equiv$\quad} l l @ {}}
-\isa{r{\isaliteral{5C3C696E76657273653E}{\isasyminverse}}} & \isa{{\isaliteral{22}{\isachardoublequote}}converse\ r{\isaliteral{22}{\isachardoublequote}}} & (\verb$^-1$)
-\end{tabular}
-\medskip
-
-\noindent
-Type synonym \ \isa{{\isaliteral{27}{\isacharprime}}a\ rel} \isa{{\isaliteral{3D}{\isacharequal}}} \isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C74696D65733E}{\isasymtimes}}\ {\isaliteral{27}{\isacharprime}}a{\isaliteral{29}{\isacharparenright}}\ set}
-
-\section{Equiv\_Relations}
-
-\begin{supertabular}{@ {} l @ {~::~} l @ {}}
-\isa{equiv} & \isa{{\isaliteral{27}{\isacharprime}}a\ set\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C74696D65733E}{\isasymtimes}}\ {\isaliteral{27}{\isacharprime}}a{\isaliteral{29}{\isacharparenright}}\ set\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ bool}\\
-\isa{op\ {\isaliteral{2F}{\isacharslash}}{\isaliteral{2F}{\isacharslash}}} & \isa{{\isaliteral{27}{\isacharprime}}a\ set\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C74696D65733E}{\isasymtimes}}\ {\isaliteral{27}{\isacharprime}}a{\isaliteral{29}{\isacharparenright}}\ set\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ set\ set}\\
-\isa{congruent} & \isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C74696D65733E}{\isasymtimes}}\ {\isaliteral{27}{\isacharprime}}a{\isaliteral{29}{\isacharparenright}}\ set\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}b{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ bool}\\
-\isa{congruent{\isadigit{2}}} & \isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C74696D65733E}{\isasymtimes}}\ {\isaliteral{27}{\isacharprime}}a{\isaliteral{29}{\isacharparenright}}\ set\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}b\ {\isaliteral{5C3C74696D65733E}{\isasymtimes}}\ {\isaliteral{27}{\isacharprime}}b{\isaliteral{29}{\isacharparenright}}\ set\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}b\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}c{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ bool}\\
-%@ {const Equiv_Relations.} & @ {term_type_only Equiv_Relations. ""}\\
-\end{supertabular}
-
-\subsubsection*{Syntax}
-
-\begin{tabular}{@ {} l @ {\quad$\equiv$\quad} l @ {}}
-\isa{f\ respects\ r} & \isa{{\isaliteral{22}{\isachardoublequote}}congruent\ r\ f{\isaliteral{22}{\isachardoublequote}}}\\
-\isa{f\ respects{\isadigit{2}}\ r} & \isa{{\isaliteral{22}{\isachardoublequote}}congruent{\isadigit{2}}\ r\ r\ f{\isaliteral{22}{\isachardoublequote}}}\\
-\end{tabular}
-
-
-\section{Transitive\_Closure}
-
-\begin{tabular}{@ {} l @ {~::~} l @ {}}
-\isa{rtrancl} & \isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C74696D65733E}{\isasymtimes}}\ {\isaliteral{27}{\isacharprime}}a{\isaliteral{29}{\isacharparenright}}\ set\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C74696D65733E}{\isasymtimes}}\ {\isaliteral{27}{\isacharprime}}a{\isaliteral{29}{\isacharparenright}}\ set}\\
-\isa{trancl} & \isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C74696D65733E}{\isasymtimes}}\ {\isaliteral{27}{\isacharprime}}a{\isaliteral{29}{\isacharparenright}}\ set\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C74696D65733E}{\isasymtimes}}\ {\isaliteral{27}{\isacharprime}}a{\isaliteral{29}{\isacharparenright}}\ set}\\
-\isa{reflcl} & \isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C74696D65733E}{\isasymtimes}}\ {\isaliteral{27}{\isacharprime}}a{\isaliteral{29}{\isacharparenright}}\ set\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C74696D65733E}{\isasymtimes}}\ {\isaliteral{27}{\isacharprime}}a{\isaliteral{29}{\isacharparenright}}\ set}\\
-\isa{acyclic} & \isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C74696D65733E}{\isasymtimes}}\ {\isaliteral{27}{\isacharprime}}a{\isaliteral{29}{\isacharparenright}}\ set\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ bool}\\
-\isa{op\ {\isaliteral{5E}{\isacharcircum}}{\isaliteral{5E}{\isacharcircum}}} & \isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C74696D65733E}{\isasymtimes}}\ {\isaliteral{27}{\isacharprime}}a{\isaliteral{29}{\isacharparenright}}\ set\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ nat\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C74696D65733E}{\isasymtimes}}\ {\isaliteral{27}{\isacharprime}}a{\isaliteral{29}{\isacharparenright}}\ set}\\
-\end{tabular}
-
-\subsubsection*{Syntax}
-
-\begin{tabular}{@ {} l @ {\quad$\equiv$\quad} l l @ {}}
-\isa{r\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}} & \isa{{\isaliteral{22}{\isachardoublequote}}rtrancl\ r{\isaliteral{22}{\isachardoublequote}}} & (\verb$^*$)\\
-\isa{r\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2B}{\isacharplus}}} & \isa{{\isaliteral{22}{\isachardoublequote}}trancl\ r{\isaliteral{22}{\isachardoublequote}}} & (\verb$^+$)\\
-\isa{r\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{3D}{\isacharequal}}} & \isa{{\isaliteral{22}{\isachardoublequote}}reflcl\ r{\isaliteral{22}{\isachardoublequote}}} & (\verb$^=$)
-\end{tabular}
-
-
-\section{Algebra}
-
-Theories \isa{Groups}, \isa{Rings}, \isa{Fields} and \isa{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 @ {}}
-\isa{{\isadigit{0}}} & \isa{{\isaliteral{27}{\isacharprime}}a}\\
-\isa{{\isadigit{1}}} & \isa{{\isaliteral{27}{\isacharprime}}a}\\
-\isa{op\ {\isaliteral{2B}{\isacharplus}}} & \isa{{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a}\\
-\isa{op\ {\isaliteral{2D}{\isacharminus}}} & \isa{{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a}\\
-\isa{uminus} & \isa{{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a} & (\verb$-$)\\
-\isa{op\ {\isaliteral{2A}{\isacharasterisk}}} & \isa{{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a}\\
-\isa{inverse} & \isa{{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a}\\
-\isa{op\ {\isaliteral{2F}{\isacharslash}}} & \isa{{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a}\\
-\isa{abs} & \isa{{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a}\\
-\isa{sgn} & \isa{{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a}\\
-\isa{op\ dvd} & \isa{{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ bool}\\
-\isa{op\ div} & \isa{{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a}\\
-\isa{op\ mod} & \isa{{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a}\\
-\end{supertabular}
-
-\subsubsection*{Syntax}
-
-\begin{tabular}{@ {} l @ {\quad$\equiv$\quad} l @ {}}
-\isa{{\isaliteral{5C3C6261723E}{\isasymbar}}x{\isaliteral{5C3C6261723E}{\isasymbar}}} & \isa{{\isaliteral{22}{\isachardoublequote}}abs\ x{\isaliteral{22}{\isachardoublequote}}}
-\end{tabular}
-
-
-\section{Nat}
-
-\isa{\isacommand{datatype}\ nat\ {\isaliteral{3D}{\isacharequal}}\ {\isadigit{0}}\ {\isaliteral{7C}{\isacharbar}}\ Suc\ nat}
-\bigskip
-
-\begin{tabular}{@ {} lllllll @ {}}
-\isa{op\ {\isaliteral{2B}{\isacharplus}}} &
-\isa{op\ {\isaliteral{2D}{\isacharminus}}} &
-\isa{op\ {\isaliteral{2A}{\isacharasterisk}}} &
-\isa{op\ {\isaliteral{5E}{\isacharcircum}}} &
-\isa{op\ div}&
-\isa{op\ mod}&
-\isa{op\ dvd}\\
-\isa{op\ {\isaliteral{5C3C6C653E}{\isasymle}}} &
-\isa{op\ {\isaliteral{3C}{\isacharless}}} &
-\isa{min} &
-\isa{max} &
-\isa{Min} &
-\isa{Max}\\
-\end{tabular}
-
-\begin{tabular}{@ {} l @ {~::~} l @ {}}
-\isa{of{\isaliteral{5F}{\isacharunderscore}}nat} & \isa{nat\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a}\\
-\isa{op\ {\isaliteral{5E}{\isacharcircum}}{\isaliteral{5E}{\isacharcircum}}} &
-  \isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ nat\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a}
-\end{tabular}
-
-\section{Int}
-
-Type \isa{int}
-\bigskip
-
-\begin{tabular}{@ {} llllllll @ {}}
-\isa{op\ {\isaliteral{2B}{\isacharplus}}} &
-\isa{op\ {\isaliteral{2D}{\isacharminus}}} &
-\isa{uminus} &
-\isa{op\ {\isaliteral{2A}{\isacharasterisk}}} &
-\isa{op\ {\isaliteral{5E}{\isacharcircum}}} &
-\isa{op\ div}&
-\isa{op\ mod}&
-\isa{op\ dvd}\\
-\isa{op\ {\isaliteral{5C3C6C653E}{\isasymle}}} &
-\isa{op\ {\isaliteral{3C}{\isacharless}}} &
-\isa{min} &
-\isa{max} &
-\isa{Min} &
-\isa{Max}\\
-\isa{abs} &
-\isa{sgn}\\
-\end{tabular}
-
-\begin{tabular}{@ {} l @ {~::~} l l @ {}}
-\isa{nat} & \isa{int\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ nat}\\
-\isa{of{\isaliteral{5F}{\isacharunderscore}}int} & \isa{int\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a}\\
-\isa{{\isaliteral{5C3C696E743E}{\isasymint}}} & \isa{{\isaliteral{27}{\isacharprime}}a\ set} & (\verb$Ints$)
-\end{tabular}
-
-\subsubsection*{Syntax}
-
-\begin{tabular}{@ {} l @ {\quad$\equiv$\quad} l @ {}}
-\isa{int} & \isa{{\isaliteral{22}{\isachardoublequote}}of{\isaliteral{5F}{\isacharunderscore}}nat{\isaliteral{22}{\isachardoublequote}}}\\
-\end{tabular}
-
-
-\section{Finite\_Set}
-
-
-\begin{supertabular}{@ {} l @ {~::~} l @ {}}
-\isa{finite} & \isa{{\isaliteral{27}{\isacharprime}}a\ set\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ bool}\\
-\isa{card} & \isa{{\isaliteral{27}{\isacharprime}}a\ set\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ nat}\\
-\isa{Finite{\isaliteral{5F}{\isacharunderscore}}Set{\isaliteral{2E}{\isachardot}}fold} & \isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}b\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}b{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}b\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ set\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}b}\\
-\isa{fold{\isaliteral{5F}{\isacharunderscore}}image} & \isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}b\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}b\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}b{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}b{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}b\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ set\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}b}\\
-\isa{setsum} & \isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}b{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ set\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}b}\\
-\isa{setprod} & \isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}b{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ set\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}b}\\
-\end{supertabular}
-
-
-\subsubsection*{Syntax}
-
-\begin{supertabular}{@ {} l @ {\quad$\equiv$\quad} l l @ {}}
-\isa{{\isaliteral{5C3C53756D3E}{\isasymSum}}A} & \isa{{\isaliteral{22}{\isachardoublequote}}setsum\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6C616D6264613E}{\isasymlambda}}x{\isaliteral{2E}{\isachardot}}\ x{\isaliteral{29}{\isacharparenright}}\ A{\isaliteral{22}{\isachardoublequote}}} & (\verb$SUM$)\\
-\isa{{\isaliteral{5C3C53756D3E}{\isasymSum}}x{\isaliteral{5C3C696E3E}{\isasymin}}A{\isaliteral{2E}{\isachardot}}\ t} & \isa{{\isaliteral{22}{\isachardoublequote}}setsum\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6C616D6264613E}{\isasymlambda}}x{\isaliteral{2E}{\isachardot}}\ t{\isaliteral{29}{\isacharparenright}}\ A{\isaliteral{22}{\isachardoublequote}}}\\
-\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C53756D3E}{\isasymSum}}x{\isaliteral{7C}{\isacharbar}}P{\isaliteral{2E}{\isachardot}}\ t{\isaliteral{22}{\isachardoublequote}}} & \isa{{\isaliteral{5C3C53756D3E}{\isasymSum}}x\ {\isaliteral{7C}{\isacharbar}}\ P{\isaliteral{2E}{\isachardot}}\ t}\\
-\multicolumn{2}{@ {}l@ {}}{Similarly for \isa{{\isaliteral{5C3C50726F643E}{\isasymProd}}} instead of \isa{{\isaliteral{5C3C53756D3E}{\isasymSum}}}} & (\verb$PROD$)\\
-\end{supertabular}
-
-
-\section{Wellfounded}
-
-\begin{supertabular}{@ {} l @ {~::~} l @ {}}
-\isa{wf} & \isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C74696D65733E}{\isasymtimes}}\ {\isaliteral{27}{\isacharprime}}a{\isaliteral{29}{\isacharparenright}}\ set\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ bool}\\
-\isa{acc} & \isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C74696D65733E}{\isasymtimes}}\ {\isaliteral{27}{\isacharprime}}a{\isaliteral{29}{\isacharparenright}}\ set\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ set}\\
-\isa{measure} & \isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ nat{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C74696D65733E}{\isasymtimes}}\ {\isaliteral{27}{\isacharprime}}a{\isaliteral{29}{\isacharparenright}}\ set}\\
-\isa{op\ {\isaliteral{3C}{\isacharless}}{\isaliteral{2A}{\isacharasterisk}}lex{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{3E}{\isachargreater}}} & \isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C74696D65733E}{\isasymtimes}}\ {\isaliteral{27}{\isacharprime}}a{\isaliteral{29}{\isacharparenright}}\ set\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}b\ {\isaliteral{5C3C74696D65733E}{\isasymtimes}}\ {\isaliteral{27}{\isacharprime}}b{\isaliteral{29}{\isacharparenright}}\ set\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C74696D65733E}{\isasymtimes}}\ {\isaliteral{27}{\isacharprime}}b{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C74696D65733E}{\isasymtimes}}\ {\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C74696D65733E}{\isasymtimes}}\ {\isaliteral{27}{\isacharprime}}b{\isaliteral{29}{\isacharparenright}}\ set}\\
-\isa{op\ {\isaliteral{3C}{\isacharless}}{\isaliteral{2A}{\isacharasterisk}}mlex{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{3E}{\isachargreater}}} & \isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ nat{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C74696D65733E}{\isasymtimes}}\ {\isaliteral{27}{\isacharprime}}a{\isaliteral{29}{\isacharparenright}}\ set\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C74696D65733E}{\isasymtimes}}\ {\isaliteral{27}{\isacharprime}}a{\isaliteral{29}{\isacharparenright}}\ set}\\
-\isa{less{\isaliteral{5F}{\isacharunderscore}}than} & \isa{{\isaliteral{28}{\isacharparenleft}}nat\ {\isaliteral{5C3C74696D65733E}{\isasymtimes}}\ nat{\isaliteral{29}{\isacharparenright}}\ set}\\
-\isa{pred{\isaliteral{5F}{\isacharunderscore}}nat} & \isa{{\isaliteral{28}{\isacharparenleft}}nat\ {\isaliteral{5C3C74696D65733E}{\isasymtimes}}\ nat{\isaliteral{29}{\isacharparenright}}\ set}\\
-\end{supertabular}
-
-
-\section{SetInterval}
-
-\begin{supertabular}{@ {} l @ {~::~} l @ {}}
-\isa{lessThan} & \isa{{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ set}\\
-\isa{atMost} & \isa{{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ set}\\
-\isa{greaterThan} & \isa{{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ set}\\
-\isa{atLeast} & \isa{{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ set}\\
-\isa{greaterThanLessThan} & \isa{{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ set}\\
-\isa{atLeastLessThan} & \isa{{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ set}\\
-\isa{greaterThanAtMost} & \isa{{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ set}\\
-\isa{atLeastAtMost} & \isa{{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ set}\\
-\end{supertabular}
-
-\subsubsection*{Syntax}
-
-\begin{supertabular}{@ {} l @ {\quad$\equiv$\quad} l @ {}}
-\isa{{\isaliteral{7B}{\isacharbraceleft}}{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}{\isaliteral{3C}{\isacharless}}y{\isaliteral{7D}{\isacharbraceright}}} & \isa{{\isaliteral{22}{\isachardoublequote}}lessThan\ y{\isaliteral{22}{\isachardoublequote}}}\\
-\isa{{\isaliteral{7B}{\isacharbraceleft}}{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}y{\isaliteral{7D}{\isacharbraceright}}} & \isa{{\isaliteral{22}{\isachardoublequote}}atMost\ y{\isaliteral{22}{\isachardoublequote}}}\\
-\isa{{\isaliteral{7B}{\isacharbraceleft}}x{\isaliteral{3C}{\isacharless}}{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}{\isaliteral{7D}{\isacharbraceright}}} & \isa{{\isaliteral{22}{\isachardoublequote}}greaterThan\ x{\isaliteral{22}{\isachardoublequote}}}\\
-\isa{{\isaliteral{7B}{\isacharbraceleft}}x{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}{\isaliteral{7D}{\isacharbraceright}}} & \isa{{\isaliteral{22}{\isachardoublequote}}atLeast\ x{\isaliteral{22}{\isachardoublequote}}}\\
-\isa{{\isaliteral{7B}{\isacharbraceleft}}x{\isaliteral{3C}{\isacharless}}{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}{\isaliteral{3C}{\isacharless}}y{\isaliteral{7D}{\isacharbraceright}}} & \isa{{\isaliteral{22}{\isachardoublequote}}greaterThanLessThan\ x\ y{\isaliteral{22}{\isachardoublequote}}}\\
-\isa{{\isaliteral{7B}{\isacharbraceleft}}x{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}{\isaliteral{3C}{\isacharless}}y{\isaliteral{7D}{\isacharbraceright}}} & \isa{{\isaliteral{22}{\isachardoublequote}}atLeastLessThan\ x\ y{\isaliteral{22}{\isachardoublequote}}}\\
-\isa{{\isaliteral{7B}{\isacharbraceleft}}x{\isaliteral{3C}{\isacharless}}{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}y{\isaliteral{7D}{\isacharbraceright}}} & \isa{{\isaliteral{22}{\isachardoublequote}}greaterThanAtMost\ x\ y{\isaliteral{22}{\isachardoublequote}}}\\
-\isa{{\isaliteral{7B}{\isacharbraceleft}}x{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}y{\isaliteral{7D}{\isacharbraceright}}} & \isa{{\isaliteral{22}{\isachardoublequote}}atLeastAtMost\ x\ y{\isaliteral{22}{\isachardoublequote}}}\\
-\isa{{\isaliteral{5C3C556E696F6E3E}{\isasymUnion}}\ i{\isaliteral{5C3C6C653E}{\isasymle}}n{\isaliteral{2E}{\isachardot}}\ A} & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C556E696F6E3E}{\isasymUnion}}\ i\ {\isaliteral{5C3C696E3E}{\isasymin}}\ {\isaliteral{7B}{\isacharbraceleft}}{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}n{\isaliteral{7D}{\isacharbraceright}}{\isaliteral{2E}{\isachardot}}\ A{\isaliteral{22}{\isachardoublequote}}}\\
-\isa{{\isaliteral{5C3C556E696F6E3E}{\isasymUnion}}\ i{\isaliteral{3C}{\isacharless}}n{\isaliteral{2E}{\isachardot}}\ A} & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C556E696F6E3E}{\isasymUnion}}\ i\ {\isaliteral{5C3C696E3E}{\isasymin}}\ {\isaliteral{7B}{\isacharbraceleft}}{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}{\isaliteral{3C}{\isacharless}}n{\isaliteral{7D}{\isacharbraceright}}{\isaliteral{2E}{\isachardot}}\ A{\isaliteral{22}{\isachardoublequote}}}\\
-\multicolumn{2}{@ {}l@ {}}{Similarly for \isa{{\isaliteral{5C3C496E7465723E}{\isasymInter}}} instead of \isa{{\isaliteral{5C3C556E696F6E3E}{\isasymUnion}}}}\\
-\isa{{\isaliteral{5C3C53756D3E}{\isasymSum}}x\ {\isaliteral{3D}{\isacharequal}}\ a{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}b{\isaliteral{2E}{\isachardot}}\ t} & \isa{{\isaliteral{22}{\isachardoublequote}}setsum\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6C616D6264613E}{\isasymlambda}}x{\isaliteral{2E}{\isachardot}}\ t{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{7B}{\isacharbraceleft}}a{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}b{\isaliteral{7D}{\isacharbraceright}}{\isaliteral{22}{\isachardoublequote}}}\\
-\isa{{\isaliteral{5C3C53756D3E}{\isasymSum}}x\ {\isaliteral{3D}{\isacharequal}}\ a{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}{\isaliteral{3C}{\isacharless}}b{\isaliteral{2E}{\isachardot}}\ t} & \isa{{\isaliteral{22}{\isachardoublequote}}setsum\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6C616D6264613E}{\isasymlambda}}x{\isaliteral{2E}{\isachardot}}\ t{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{7B}{\isacharbraceleft}}a{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}{\isaliteral{3C}{\isacharless}}b{\isaliteral{7D}{\isacharbraceright}}{\isaliteral{22}{\isachardoublequote}}}\\
-\isa{{\isaliteral{5C3C53756D3E}{\isasymSum}}x{\isaliteral{5C3C6C653E}{\isasymle}}b{\isaliteral{2E}{\isachardot}}\ t} & \isa{{\isaliteral{22}{\isachardoublequote}}setsum\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6C616D6264613E}{\isasymlambda}}x{\isaliteral{2E}{\isachardot}}\ t{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{7B}{\isacharbraceleft}}{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}b{\isaliteral{7D}{\isacharbraceright}}{\isaliteral{22}{\isachardoublequote}}}\\
-\isa{{\isaliteral{5C3C53756D3E}{\isasymSum}}x{\isaliteral{3C}{\isacharless}}b{\isaliteral{2E}{\isachardot}}\ t} & \isa{{\isaliteral{22}{\isachardoublequote}}setsum\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6C616D6264613E}{\isasymlambda}}x{\isaliteral{2E}{\isachardot}}\ t{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{7B}{\isacharbraceleft}}{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}{\isaliteral{3C}{\isacharless}}b{\isaliteral{7D}{\isacharbraceright}}{\isaliteral{22}{\isachardoublequote}}}\\
-\multicolumn{2}{@ {}l@ {}}{Similarly for \isa{{\isaliteral{5C3C50726F643E}{\isasymProd}}} instead of \isa{{\isaliteral{5C3C53756D3E}{\isasymSum}}}}\\
-\end{supertabular}
-
-
-\section{Power}
-
-\begin{tabular}{@ {} l @ {~::~} l @ {}}
-\isa{op\ {\isaliteral{5E}{\isacharcircum}}} & \isa{{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ nat\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a}
-\end{tabular}
-
-
-\section{Option}
-
-\isa{\isacommand{datatype}\ {\isaliteral{27}{\isacharprime}}a\ option\ {\isaliteral{3D}{\isacharequal}}\ None\ {\isaliteral{7C}{\isacharbar}}\ Some\ {\isaliteral{27}{\isacharprime}}a}
-\bigskip
-
-\begin{tabular}{@ {} l @ {~::~} l @ {}}
-\isa{the} & \isa{{\isaliteral{27}{\isacharprime}}a\ option\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a}\\
-\isa{Option{\isaliteral{2E}{\isachardot}}map} & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}b{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ option\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}b\ option{\isaliteral{22}{\isachardoublequote}}}\\
-\isa{Option{\isaliteral{2E}{\isachardot}}set} & \isa{{\isaliteral{27}{\isacharprime}}a\ option\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ set}\\
-\isa{Option{\isaliteral{2E}{\isachardot}}bind} & \isa{{\isaliteral{27}{\isacharprime}}a\ option\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}b\ option{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}b\ option}
-\end{tabular}
-
-\section{List}
-
-\isa{\isacommand{datatype}\ {\isaliteral{27}{\isacharprime}}a\ list\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{7C}{\isacharbar}}\ op\ {\isaliteral{23}{\isacharhash}}\ {\isaliteral{27}{\isacharprime}}a\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ list{\isaliteral{29}{\isacharparenright}}}
-\bigskip
-
-\begin{supertabular}{@ {} l @ {~::~} l @ {}}
-\isa{op\ {\isaliteral{40}{\isacharat}}} & \isa{{\isaliteral{27}{\isacharprime}}a\ list\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ list\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ list}\\
-\isa{butlast} & \isa{{\isaliteral{27}{\isacharprime}}a\ list\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ list}\\
-\isa{concat} & \isa{{\isaliteral{27}{\isacharprime}}a\ list\ list\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ list}\\
-\isa{distinct} & \isa{{\isaliteral{27}{\isacharprime}}a\ list\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ bool}\\
-\isa{drop} & \isa{nat\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ list\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ list}\\
-\isa{dropWhile} & \isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ bool{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ list\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ list}\\
-\isa{filter} & \isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ bool{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ list\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ list}\\
-\isa{List{\isaliteral{2E}{\isachardot}}find} & \isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ bool{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ list\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ option}\\
-\isa{fold} & \isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}b\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}b{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ list\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}b\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}b}\\
-\isa{foldr} & \isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}b\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}b{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ list\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}b\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}b}\\
-\isa{foldl} & \isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}b\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}b\ list\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a}\\
-\isa{hd} & \isa{{\isaliteral{27}{\isacharprime}}a\ list\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a}\\
-\isa{last} & \isa{{\isaliteral{27}{\isacharprime}}a\ list\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a}\\
-\isa{length} & \isa{{\isaliteral{27}{\isacharprime}}a\ list\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ nat}\\
-\isa{lenlex} & \isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C74696D65733E}{\isasymtimes}}\ {\isaliteral{27}{\isacharprime}}a{\isaliteral{29}{\isacharparenright}}\ set\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ list\ {\isaliteral{5C3C74696D65733E}{\isasymtimes}}\ {\isaliteral{27}{\isacharprime}}a\ list{\isaliteral{29}{\isacharparenright}}\ set}\\
-\isa{lex} & \isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C74696D65733E}{\isasymtimes}}\ {\isaliteral{27}{\isacharprime}}a{\isaliteral{29}{\isacharparenright}}\ set\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ list\ {\isaliteral{5C3C74696D65733E}{\isasymtimes}}\ {\isaliteral{27}{\isacharprime}}a\ list{\isaliteral{29}{\isacharparenright}}\ set}\\
-\isa{lexn} & \isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C74696D65733E}{\isasymtimes}}\ {\isaliteral{27}{\isacharprime}}a{\isaliteral{29}{\isacharparenright}}\ set\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ nat\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ list\ {\isaliteral{5C3C74696D65733E}{\isasymtimes}}\ {\isaliteral{27}{\isacharprime}}a\ list{\isaliteral{29}{\isacharparenright}}\ set}\\
-\isa{lexord} & \isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C74696D65733E}{\isasymtimes}}\ {\isaliteral{27}{\isacharprime}}a{\isaliteral{29}{\isacharparenright}}\ set\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ list\ {\isaliteral{5C3C74696D65733E}{\isasymtimes}}\ {\isaliteral{27}{\isacharprime}}a\ list{\isaliteral{29}{\isacharparenright}}\ set}\\
-\isa{listrel} & \isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C74696D65733E}{\isasymtimes}}\ {\isaliteral{27}{\isacharprime}}b{\isaliteral{29}{\isacharparenright}}\ set\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ list\ {\isaliteral{5C3C74696D65733E}{\isasymtimes}}\ {\isaliteral{27}{\isacharprime}}b\ list{\isaliteral{29}{\isacharparenright}}\ set}\\
-\isa{listrel{\isadigit{1}}} & \isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C74696D65733E}{\isasymtimes}}\ {\isaliteral{27}{\isacharprime}}a{\isaliteral{29}{\isacharparenright}}\ set\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ list\ {\isaliteral{5C3C74696D65733E}{\isasymtimes}}\ {\isaliteral{27}{\isacharprime}}a\ list{\isaliteral{29}{\isacharparenright}}\ set}\\
-\isa{lists} & \isa{{\isaliteral{27}{\isacharprime}}a\ set\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ list\ set}\\
-\isa{listset} & \isa{{\isaliteral{27}{\isacharprime}}a\ set\ list\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ list\ set}\\
-\isa{listsum} & \isa{{\isaliteral{27}{\isacharprime}}a\ list\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a}\\
-\isa{list{\isaliteral{5F}{\isacharunderscore}}all{\isadigit{2}}} & \isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}b\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ bool{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ list\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}b\ list\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ bool}\\
-\isa{list{\isaliteral{5F}{\isacharunderscore}}update} & \isa{{\isaliteral{27}{\isacharprime}}a\ list\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ nat\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ list}\\
-\isa{map} & \isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}b{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ list\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}b\ list}\\
-\isa{measures} & \isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ nat{\isaliteral{29}{\isacharparenright}}\ list\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C74696D65733E}{\isasymtimes}}\ {\isaliteral{27}{\isacharprime}}a{\isaliteral{29}{\isacharparenright}}\ set}\\
-\isa{op\ {\isaliteral{21}{\isacharbang}}} & \isa{{\isaliteral{27}{\isacharprime}}a\ list\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ nat\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a}\\
-\isa{remdups} & \isa{{\isaliteral{27}{\isacharprime}}a\ list\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ list}\\
-\isa{removeAll} & \isa{{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ list\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ list}\\
-\isa{remove{\isadigit{1}}} & \isa{{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ list\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ list}\\
-\isa{replicate} & \isa{nat\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ list}\\
-\isa{rev} & \isa{{\isaliteral{27}{\isacharprime}}a\ list\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ list}\\
-\isa{rotate} & \isa{nat\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ list\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ list}\\
-\isa{rotate{\isadigit{1}}} & \isa{{\isaliteral{27}{\isacharprime}}a\ list\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ list}\\
-\isa{set} & \isa{{\isaliteral{27}{\isacharprime}}a\ list\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ set}\\
-\isa{sort} & \isa{{\isaliteral{27}{\isacharprime}}a\ list\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ list}\\
-\isa{sorted} & \isa{{\isaliteral{27}{\isacharprime}}a\ list\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ bool}\\
-\isa{splice} & \isa{{\isaliteral{27}{\isacharprime}}a\ list\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ list\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ list}\\
-\isa{sublist} & \isa{{\isaliteral{27}{\isacharprime}}a\ list\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ nat\ set\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ list}\\
-\isa{take} & \isa{nat\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ list\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ list}\\
-\isa{takeWhile} & \isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ bool{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ list\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ list}\\
-\isa{tl} & \isa{{\isaliteral{27}{\isacharprime}}a\ list\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ list}\\
-\isa{upt} & \isa{nat\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ nat\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ nat\ list}\\
-\isa{upto} & \isa{int\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ int\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ int\ list}\\
-\isa{zip} & \isa{{\isaliteral{27}{\isacharprime}}a\ list\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}b\ list\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C74696D65733E}{\isasymtimes}}\ {\isaliteral{27}{\isacharprime}}b{\isaliteral{29}{\isacharparenright}}\ list}\\
-\end{supertabular}
-
-\subsubsection*{Syntax}
-
-\begin{supertabular}{@ {} l @ {\quad$\equiv$\quad} l @ {}}
-\isa{{\isaliteral{5B}{\isacharbrackleft}}x\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}x\isaliteral{5C3C5E697375623E}{}\isactrlisub n{\isaliteral{5D}{\isacharbrackright}}} & \isa{x\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}\ {\isaliteral{23}{\isacharhash}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ {\isaliteral{23}{\isacharhash}}\ x\isaliteral{5C3C5E697375623E}{}\isactrlisub n\ {\isaliteral{23}{\isacharhash}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}}\\
-\isa{{\isaliteral{5B}{\isacharbrackleft}}m{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}{\isaliteral{3C}{\isacharless}}n{\isaliteral{5D}{\isacharbrackright}}} & \isa{{\isaliteral{22}{\isachardoublequote}}upt\ m\ n{\isaliteral{22}{\isachardoublequote}}}\\
-\isa{{\isaliteral{5B}{\isacharbrackleft}}i{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}j{\isaliteral{5D}{\isacharbrackright}}} & \isa{{\isaliteral{22}{\isachardoublequote}}upto\ i\ j{\isaliteral{22}{\isachardoublequote}}}\\
-\isa{{\isaliteral{5B}{\isacharbrackleft}}e{\isaliteral{2E}{\isachardot}}\ x\ {\isaliteral{5C3C6C6566746172726F773E}{\isasymleftarrow}}\ xs{\isaliteral{5D}{\isacharbrackright}}} & \isa{map\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6C616D6264613E}{\isasymlambda}}x{\isaliteral{2E}{\isachardot}}\ e{\isaliteral{29}{\isacharparenright}}\ xs}\\
-\isa{{\isaliteral{5B}{\isacharbrackleft}}x{\isaliteral{5C3C6C6566746172726F773E}{\isasymleftarrow}}xs\ {\isaliteral{2E}{\isachardot}}\ b{\isaliteral{5D}{\isacharbrackright}}} & \isa{{\isaliteral{22}{\isachardoublequote}}filter\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6C616D6264613E}{\isasymlambda}}x{\isaliteral{2E}{\isachardot}}\ b{\isaliteral{29}{\isacharparenright}}\ xs{\isaliteral{22}{\isachardoublequote}}} \\
-\isa{xs{\isaliteral{5B}{\isacharbrackleft}}n\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3D}{\isacharequal}}\ x{\isaliteral{5D}{\isacharbrackright}}} & \isa{{\isaliteral{22}{\isachardoublequote}}list{\isaliteral{5F}{\isacharunderscore}}update\ xs\ n\ x{\isaliteral{22}{\isachardoublequote}}}\\
-\isa{{\isaliteral{5C3C53756D3E}{\isasymSum}}x{\isaliteral{5C3C6C6566746172726F773E}{\isasymleftarrow}}xs{\isaliteral{2E}{\isachardot}}\ e} & \isa{{\isaliteral{22}{\isachardoublequote}}listsum\ {\isaliteral{28}{\isacharparenleft}}map\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6C616D6264613E}{\isasymlambda}}x{\isaliteral{2E}{\isachardot}}\ e{\isaliteral{29}{\isacharparenright}}\ xs{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}}\\
-\end{supertabular}
-\medskip
-
-List comprehension: \isa{{\isaliteral{5B}{\isacharbrackleft}}e{\isaliteral{2E}{\isachardot}}\ q\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}\ q\isaliteral{5C3C5E697375623E}{}\isactrlisub n{\isaliteral{5D}{\isacharbrackright}}} where each
-qualifier \isa{q\isaliteral{5C3C5E697375623E}{}\isactrlisub i} is either a generator \mbox{\isa{pat\ {\isaliteral{5C3C6C6566746172726F773E}{\isasymleftarrow}}\ 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{supertabular}{@ {} l @ {~::~} l @ {}}
-\isa{Map{\isaliteral{2E}{\isachardot}}empty} & \isa{{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}b\ option}\\
-\isa{op\ {\isaliteral{2B}{\isacharplus}}{\isaliteral{2B}{\isacharplus}}} & \isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}b\ option{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}b\ option{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}b\ option}\\
-\isa{op\ {\isaliteral{5C3C636972633E}{\isasymcirc}}\isaliteral{5C3C5E7375623E}{}\isactrlsub m} & \isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}b\ option{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}c\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ option{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}c\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}b\ option}\\
-\isa{op\ {\isaliteral{7C}{\isacharbar}}{\isaliteral{60}{\isacharbackquote}}} & \isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}b\ option{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ set\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}b\ option}\\
-\isa{dom} & \isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}b\ option{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ set}\\
-\isa{ran} & \isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}b\ option{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}b\ set}\\
-\isa{op\ {\isaliteral{5C3C73756273657465713E}{\isasymsubseteq}}\isaliteral{5C3C5E7375623E}{}\isactrlsub m} & \isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}b\ option{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}b\ option{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ bool}\\
-\isa{map{\isaliteral{5F}{\isacharunderscore}}of} & \isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C74696D65733E}{\isasymtimes}}\ {\isaliteral{27}{\isacharprime}}b{\isaliteral{29}{\isacharparenright}}\ list\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}b\ option}\\
-\isa{map{\isaliteral{5F}{\isacharunderscore}}upds} & \isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}b\ option{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ list\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}b\ list\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}b\ option}\\
-\end{supertabular}
-
-\subsubsection*{Syntax}
-
-\begin{tabular}{@ {} l @ {\quad$\equiv$\quad} l @ {}}
-\isa{Map{\isaliteral{2E}{\isachardot}}empty} & \isa{{\isaliteral{5C3C6C616D6264613E}{\isasymlambda}}x{\isaliteral{2E}{\isachardot}}\ None}\\
-\isa{m{\isaliteral{28}{\isacharparenleft}}x\ {\isaliteral{5C3C6D617073746F3E}{\isasymmapsto}}\ y{\isaliteral{29}{\isacharparenright}}} & \isa{{\isaliteral{22}{\isachardoublequote}}m{\isaliteral{28}{\isacharparenleft}}x{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3D}{\isacharequal}}Some\ y{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}}\\
-\isa{m{\isaliteral{28}{\isacharparenleft}}x\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}{\isaliteral{5C3C6D617073746F3E}{\isasymmapsto}}y\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}x\isaliteral{5C3C5E697375623E}{}\isactrlisub n{\isaliteral{5C3C6D617073746F3E}{\isasymmapsto}}y\isaliteral{5C3C5E697375623E}{}\isactrlisub n{\isaliteral{29}{\isacharparenright}}} & \isa{{\isaliteral{22}{\isachardoublequote}}m{\isaliteral{28}{\isacharparenleft}}x\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}{\isaliteral{5C3C6D617073746F3E}{\isasymmapsto}}y\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{28}{\isacharparenleft}}x\isaliteral{5C3C5E697375623E}{}\isactrlisub n{\isaliteral{5C3C6D617073746F3E}{\isasymmapsto}}y\isaliteral{5C3C5E697375623E}{}\isactrlisub n{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}}\\
-\isa{{\isaliteral{5B}{\isacharbrackleft}}x\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}{\isaliteral{5C3C6D617073746F3E}{\isasymmapsto}}y\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}x\isaliteral{5C3C5E697375623E}{}\isactrlisub n{\isaliteral{5C3C6D617073746F3E}{\isasymmapsto}}y\isaliteral{5C3C5E697375623E}{}\isactrlisub n{\isaliteral{5D}{\isacharbrackright}}} & \isa{{\isaliteral{22}{\isachardoublequote}}Map{\isaliteral{2E}{\isachardot}}empty{\isaliteral{28}{\isacharparenleft}}x\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}{\isaliteral{5C3C6D617073746F3E}{\isasymmapsto}}y\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}x\isaliteral{5C3C5E697375623E}{}\isactrlisub n{\isaliteral{5C3C6D617073746F3E}{\isasymmapsto}}y\isaliteral{5C3C5E697375623E}{}\isactrlisub n{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}}\\
-\isa{m{\isaliteral{28}{\isacharparenleft}}xs\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5C3C6D617073746F3E}{\isasymmapsto}}{\isaliteral{5D}{\isacharbrackright}}\ ys{\isaliteral{29}{\isacharparenright}}} & \isa{{\isaliteral{22}{\isachardoublequote}}map{\isaliteral{5F}{\isacharunderscore}}upds\ m\ xs\ ys{\isaliteral{22}{\isachardoublequote}}}\\
-\end{tabular}%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isadelimtheory
-%
-\endisadelimtheory
-%
-\isatagtheory
-%
-\endisatagtheory
-{\isafoldtheory}%
-%
-\isadelimtheory
-%
-\endisadelimtheory
-\end{isabellebody}%
-%%% Local Variables:
-%%% mode: latex
-%%% TeX-master: "root"
-%%% End:

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Main/Main_Doc.thy	Mon Aug 27 21:30:18 2012 +0200
@@ -0,0 +1,596 @@
+(*<*)
+theory Main_Doc
+imports Main
+begin
+
+setup {*
+  let
+    fun pretty_term_type_only ctxt (t, T) =
+      (if fastype_of t = Sign.certify_typ (Proof_Context.theory_of ctxt) T then ()
+       else error "term_type_only: type mismatch";
+       Syntax.pretty_typ ctxt T)
+  in
+    Thy_Output.antiquotation @{binding term_type_only}
+      (Args.term -- Args.typ_abbrev)
+      (fn {source, context = ctxt, ...} => fn arg =>
+        Thy_Output.output ctxt
+          (Thy_Output.maybe_pretty_source pretty_term_type_only ctxt source [arg]))
+  end
+*}
+setup {*
+  Thy_Output.antiquotation @{binding expanded_typ} (Args.typ >> single)
+    (fn {source, context, ...} => Thy_Output.output context o
+      Thy_Output.maybe_pretty_source Syntax.pretty_typ context source)
+*}
+(*>*)
+text{*
+
+\begin{abstract}
+This document lists the main types, functions and syntax provided by theory @{theory Main}. It is meant as a quick overview of what is available. The sophisticated class structure is only hinted at. For details see \url{http://isabelle.in.tum.de/library/HOL/}.
+\end{abstract}
+
+\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"}.
+\smallskip
+
+\begin{tabular}{@ {} l @ {~::~} l @ {}}
+@{const HOL.undefined} & @{typeof HOL.undefined}\\
+@{const HOL.default} & @{typeof HOL.default}\\
+\end{tabular}
+
+\subsubsection*{Syntax}
+
+\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 @ {}}
+@{const Orderings.less_eq} & @{typeof Orderings.less_eq} & (\verb$<=$)\\
+@{const Orderings.less} & @{typeof Orderings.less}\\
+@{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 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"}\\
+@{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}
+
+
+\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 Complete_Lattices.Inf} & @{term_type_only Complete_Lattices.Inf "'a set \<Rightarrow> 'a::Inf"}\\
+@{const Complete_Lattices.Sup} & @{term_type_only Complete_Lattices.Sup "'a set \<Rightarrow> 'a::Sup"}\\
+\end{tabular}
+
+\subsubsection*{Syntax}
+
+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"}\\
+@{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"}\\
+@{text[source]"\<top>"} & @{term[source] top}\\
+@{text[source]"\<bottom>"} & @{term[source] bot}\\
+\end{supertabular}
+
+
+\section{Set}
+
+%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"}\\
+@{const Set.member} & @{term_type_only Set.member "'a\<Rightarrow>'a set\<Rightarrow>bool"} & (\texttt{:})\\
+@{const Set.union} & @{term_type_only Set.union "'a set\<Rightarrow>'a set \<Rightarrow> 'a set"} & (\texttt{Un})\\
+@{const Set.inter} & @{term_type_only Set.inter "'a set\<Rightarrow>'a set \<Rightarrow> 'a set"} & (\texttt{Int})\\
+@{const UNION} & @{term_type_only UNION "'a set\<Rightarrow>('a \<Rightarrow> 'b set) \<Rightarrow> 'b set"}\\
+@{const INTER} & @{term_type_only INTER "'a set\<Rightarrow>('a \<Rightarrow> 'b set) \<Rightarrow> 'b set"}\\
+@{const Union} & @{term_type_only Union "'a set set\<Rightarrow>'a set"}\\
+@{const Inter} & @{term_type_only Inter "'a set set\<Rightarrow>'a set"}\\
+@{const Pow} & @{term_type_only Pow "'a set \<Rightarrow>'a set set"}\\
+@{const UNIV} & @{term_type_only UNIV "'a set"}\\
+@{const image} & @{term_type_only image "('a\<Rightarrow>'b)\<Rightarrow>'a set\<Rightarrow>'b set"}\\
+@{const Ball} & @{term_type_only Ball "'a set\<Rightarrow>('a\<Rightarrow>bool)\<Rightarrow>bool"}\\
+@{const Bex} & @{term_type_only Bex "'a set\<Rightarrow>('a\<Rightarrow>bool)\<Rightarrow>bool"}\\
+\end{supertabular}
+
+\subsubsection*{Syntax}
+
+\begin{supertabular}{@ {} l @ {\quad$\equiv$\quad} l l @ {}}
+@{text"{x\<^isub>1,\<dots>,x\<^isub>n}"} & @{text"insert x\<^isub>1 (\<dots> (insert x\<^isub>n {})\<dots>)"}\\
+@{term"x ~: A"} & @{term[source]"\<not>(x \<in> A)"}\\
+@{term"A \<subseteq> B"} & @{term[source]"A \<le> B"}\\
+@{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[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})\\
+@{term[mode=xsymbols]"INT x. A"} & @{term[source]"INTER UNIV (\<lambda>x. A)"}\\
+@{term"ALL x:A. P"} & @{term[source]"Ball A (\<lambda>x. P)"}\\
+@{term"EX x:A. P"} & @{term[source]"Bex A (\<lambda>x. P)"}\\
+@{term"range f"} & @{term[source]"f ` UNIV"}\\
+\end{supertabular}
+
+
+\section{Fun}
+
+\begin{supertabular}{@ {} l @ {~::~} l l @ {}}
+@{const "Fun.id"} & @{typeof Fun.id}\\
+@{const "Fun.comp"} & @{typeof Fun.comp} & (\texttt{o})\\
+@{const "Fun.inj_on"} & @{term_type_only Fun.inj_on "('a\<Rightarrow>'b)\<Rightarrow>'a set\<Rightarrow>bool"}\\
+@{const "Fun.inj"} & @{typeof Fun.inj}\\
+@{const "Fun.surj"} & @{typeof Fun.surj}\\
+@{const "Fun.bij"} & @{typeof Fun.bij}\\
+@{const "Fun.bij_betw"} & @{term_type_only Fun.bij_betw "('a\<Rightarrow>'b)\<Rightarrow>'a set\<Rightarrow>'b set\<Rightarrow>bool"}\\
+@{const "Fun.fun_upd"} & @{typeof Fun.fun_upd}\\
+\end{supertabular}
+
+\subsubsection*{Syntax}
+
+\begin{tabular}{@ {} l @ {\quad$\equiv$\quad} l @ {}}
+@{term"fun_upd f x y"} & @{term[source]"fun_upd f x y"}\\
+@{text"f(x\<^isub>1:=y\<^isub>1,\<dots>,x\<^isub>n:=y\<^isub>n)"} & @{text"f(x\<^isub>1:=y\<^isub>1)\<dots>(x\<^isub>n:=y\<^isub>n)"}\\
+\end{tabular}
+
+
+\section{Hilbert\_Choice}
+
+Hilbert's selection ($\varepsilon$) operator: @{term"SOME x. P"}.
+\smallskip
+
+\begin{tabular}{@ {} l @ {~::~} l @ {}}
+@{const Hilbert_Choice.inv_into} & @{term_type_only Hilbert_Choice.inv_into "'a set \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> ('b \<Rightarrow> 'a)"}
+\end{tabular}
+
+\subsubsection*{Syntax}
+
+\begin{tabular}{@ {} l @ {\quad$\equiv$\quad} l @ {}}
+@{term inv} & @{term[source]"inv_into UNIV"}
+\end{tabular}
+
+\section{Fixed Points}
+
+Theory: @{theory Inductive}.
+
+Least and greatest fixed points in a complete lattice @{typ 'a}:
+
+\begin{tabular}{@ {} l @ {~::~} l @ {}}
+@{const Inductive.lfp} & @{typeof Inductive.lfp}\\
+@{const Inductive.gfp} & @{typeof Inductive.gfp}\\
+\end{tabular}
+
+Note that in particular sets (@{typ"'a \<Rightarrow> bool"}) are complete lattices.
+
+\section{Sum\_Type}
+
+Type constructor @{text"+"}.
+
+\begin{tabular}{@ {} l @ {~::~} l @ {}}
+@{const Sum_Type.Inl} & @{typeof Sum_Type.Inl}\\
+@{const Sum_Type.Inr} & @{typeof Sum_Type.Inr}\\
+@{const Sum_Type.Plus} & @{term_type_only Sum_Type.Plus "'a set\<Rightarrow>'b set\<Rightarrow>('a+'b)set"}
+\end{tabular}
+
+
+\section{Product\_Type}
+
+Types @{typ unit} and @{text"\<times>"}.
+
+\begin{supertabular}{@ {} l @ {~::~} l @ {}}
+@{const Product_Type.Unity} & @{typeof Product_Type.Unity}\\
+@{const Pair} & @{typeof Pair}\\
+@{const fst} & @{typeof fst}\\
+@{const snd} & @{typeof snd}\\
+@{const split} & @{typeof split}\\
+@{const curry} & @{typeof curry}\\
+@{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} 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 \mbox{@{text"(a, (b, c))"}.}
+Pattern matching with pairs and tuples extends to all binders,
+e.g.\ \mbox{@{prop"ALL (x,y):A. P"},} @{term"{(x,y). P}"}, etc.
+
+
+\section{Relation}
+
+\begin{tabular}{@ {} l @ {~::~} l @ {}}
+@{const Relation.converse} & @{term_type_only Relation.converse "('a * 'b)set \<Rightarrow> ('b*'a)set"}\\
+@{const Relation.relcomp} & @{term_type_only Relation.relcomp "('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.Id} & @{term_type_only Relation.Id "('a*'a)set"}\\
+@{const Relation.Domain} & @{term_type_only Relation.Domain "('a*'b)set\<Rightarrow>'a set"}\\
+@{const Relation.Range} & @{term_type_only Relation.Range "('a*'b)set\<Rightarrow>'b set"}\\
+@{const Relation.Field} & @{term_type_only Relation.Field "('a*'a)set\<Rightarrow>'a set"}\\
+@{const Relation.refl_on} & @{term_type_only Relation.refl_on "'a set\<Rightarrow>('a*'a)set\<Rightarrow>bool"}\\
+@{const Relation.refl} & @{term_type_only Relation.refl "('a*'a)set\<Rightarrow>bool"}\\
+@{const Relation.sym} & @{term_type_only Relation.sym "('a*'a)set\<Rightarrow>bool"}\\
+@{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{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"="} @{expanded_typ "'a rel"}
+
+\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"}\\
+@{const Equiv_Relations.quotient} & @{term_type_only Equiv_Relations.quotient "'a set \<Rightarrow> ('a \<times> 'a) set \<Rightarrow> 'a set set"}\\
+@{const Equiv_Relations.congruent} & @{term_type_only Equiv_Relations.congruent "('a*'a)set\<Rightarrow>('a\<Rightarrow>'b)\<Rightarrow>bool"}\\
+@{const Equiv_Relations.congruent2} & @{term_type_only Equiv_Relations.congruent2 "('a*'a)set\<Rightarrow>('b*'b)set\<Rightarrow>('a\<Rightarrow>'b\<Rightarrow>'c)\<Rightarrow>bool"}\\
+%@ {const Equiv_Relations.} & @ {term_type_only Equiv_Relations. ""}\\
+\end{supertabular}
+
+\subsubsection*{Syntax}
+
+\begin{tabular}{@ {} l @ {\quad$\equiv$\quad} l @ {}}
+@{term"congruent r f"} & @{term[source]"congruent r f"}\\
+@{term"congruent2 r r f"} & @{term[source]"congruent2 r r f"}\\
+\end{tabular}
+
+
+\section{Transitive\_Closure}
+
+\begin{tabular}{@ {} l @ {~::~} l @ {}}
+@{const Transitive_Closure.rtrancl} & @{term_type_only Transitive_Closure.rtrancl "('a*'a)set\<Rightarrow>('a*'a)set"}\\
+@{const Transitive_Closure.trancl} & @{term_type_only Transitive_Closure.trancl "('a*'a)set\<Rightarrow>('a*'a)set"}\\
+@{const Transitive_Closure.reflcl} & @{term_type_only Transitive_Closure.reflcl "('a*'a)set\<Rightarrow>('a*'a)set"}\\
+@{const Transitive_Closure.acyclic} & @{term_type_only Transitive_Closure.acyclic "('a*'a)set\<Rightarrow>bool"}\\
+@{const compower} & @{term_type_only "op ^^ :: ('a*'a)set\<Rightarrow>nat\<Rightarrow>('a*'a)set" "('a*'a)set\<Rightarrow>nat\<Rightarrow>('a*'a)set"}\\
+\end{tabular}
+
+\subsubsection*{Syntax}
+
+\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 Groups}, @{theory Rings}, @{theory Fields} 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}
+
+@{datatype nat}
+\bigskip
+
+\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"} &
+@{term "min :: nat \<Rightarrow> nat \<Rightarrow> nat"} &
+@{term "max :: nat \<Rightarrow> nat \<Rightarrow> nat"} &
+@{term "Min :: nat set \<Rightarrow> nat"} &
+@{term "Max :: nat set \<Rightarrow> nat"}\\
+\end{tabular}
+
+\begin{tabular}{@ {} l @ {~::~} l @ {}}
+@{const Nat.of_nat} & @{typeof Nat.of_nat}\\
+@{term "op ^^ :: ('a \<Rightarrow> 'a) \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> 'a"} &
+  @{term_type_only "op ^^ :: ('a \<Rightarrow> 'a) \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> 'a" "('a \<Rightarrow> 'a) \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> 'a"}
+\end{tabular}
+
+\section{Int}
+
+Type @{typ int}
+\bigskip
+
+\begin{tabular}{@ {} llllllll @ {}}
+@{term "op + :: int \<Rightarrow> int \<Rightarrow> int"} &
+@{term "op - :: int \<Rightarrow> int \<Rightarrow> int"} &
+@{term "uminus :: int \<Rightarrow> int"} &
+@{term "op * :: int \<Rightarrow> int \<Rightarrow> int"} &
+@{term "op ^ :: int \<Rightarrow> nat \<Rightarrow> int"} &
+@{term "op div :: int \<Rightarrow> int \<Rightarrow> int"}&
+@{term "op mod :: int \<Rightarrow> int \<Rightarrow> int"}&
+@{term "op dvd :: int \<Rightarrow> int \<Rightarrow> bool"}\\
+@{term "op \<le> :: int \<Rightarrow> int \<Rightarrow> bool"} &
+@{term "op < :: int \<Rightarrow> int \<Rightarrow> bool"} &
+@{term "min :: int \<Rightarrow> int \<Rightarrow> int"} &
+@{term "max :: int \<Rightarrow> int \<Rightarrow> int"} &
+@{term "Min :: int set \<Rightarrow> int"} &
+@{term "Max :: int set \<Rightarrow> int"}\\
+@{term "abs :: int \<Rightarrow> int"} &
+@{term "sgn :: int \<Rightarrow> int"}\\
+\end{tabular}
+
+\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"} & (\verb$Ints$)
+\end{tabular}
+
+\subsubsection*{Syntax}
+
+\begin{tabular}{@ {} l @ {\quad$\equiv$\quad} l @ {}}
+@{term"of_nat::nat\<Rightarrow>int"} & @{term[source]"of_nat"}\\
+\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 Big_Operators.setsum} & @{term_type_only Big_Operators.setsum "('a => 'b) => 'a set => 'b::comm_monoid_add"}\\
+@{const Big_Operators.setprod} & @{term_type_only Big_Operators.setprod "('a => 'b) => 'a set => 'b::comm_monoid_mult"}\\
+\end{supertabular}
+
+
+\subsubsection*{Syntax}
+
+\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>"}} & (\verb$PROD$)\\
+\end{supertabular}
+
+
+\section{Wellfounded}
+
+\begin{supertabular}{@ {} l @ {~::~} l @ {}}
+@{const Wellfounded.wf} & @{term_type_only Wellfounded.wf "('a*'a)set\<Rightarrow>bool"}\\
+@{const Wellfounded.acc} & @{term_type_only Wellfounded.acc "('a*'a)set\<Rightarrow>'a set"}\\
+@{const Wellfounded.measure} & @{term_type_only Wellfounded.measure "('a\<Rightarrow>nat)\<Rightarrow>('a*'a)set"}\\
+@{const Wellfounded.lex_prod} & @{term_type_only Wellfounded.lex_prod "('a*'a)set\<Rightarrow>('b*'b)set\<Rightarrow>(('a*'b)*('a*'b))set"}\\
+@{const Wellfounded.mlex_prod} & @{term_type_only Wellfounded.mlex_prod "('a\<Rightarrow>nat)\<Rightarrow>('a*'a)set\<Rightarrow>('a*'a)set"}\\
+@{const Wellfounded.less_than} & @{term_type_only Wellfounded.less_than "(nat*nat)set"}\\
+@{const Wellfounded.pred_nat} & @{term_type_only Wellfounded.pred_nat "(nat*nat)set"}\\
+\end{supertabular}
+
+
+\section{SetInterval}
+
+\begin{supertabular}{@ {} l @ {~::~} l @ {}}
+@{const lessThan} & @{term_type_only lessThan "'a::ord \<Rightarrow> 'a set"}\\
+@{const atMost} & @{term_type_only atMost "'a::ord \<Rightarrow> 'a set"}\\
+@{const greaterThan} & @{term_type_only greaterThan "'a::ord \<Rightarrow> 'a set"}\\
+@{const atLeast} & @{term_type_only atLeast "'a::ord \<Rightarrow> 'a set"}\\
+@{const greaterThanLessThan} & @{term_type_only greaterThanLessThan "'a::ord \<Rightarrow> 'a \<Rightarrow> 'a set"}\\
+@{const atLeastLessThan} & @{term_type_only atLeastLessThan "'a::ord \<Rightarrow> 'a \<Rightarrow> 'a set"}\\
+@{const greaterThanAtMost} & @{term_type_only greaterThanAtMost "'a::ord \<Rightarrow> 'a \<Rightarrow> 'a set"}\\
+@{const atLeastAtMost} & @{term_type_only atLeastAtMost "'a::ord \<Rightarrow> 'a \<Rightarrow> 'a set"}\\
+\end{supertabular}
+
+\subsubsection*{Syntax}
+
+\begin{supertabular}{@ {} l @ {\quad$\equiv$\quad} l @ {}}
+@{term "lessThan y"} & @{term[source] "lessThan y"}\\
+@{term "atMost y"} & @{term[source] "atMost y"}\\
+@{term "greaterThan x"} & @{term[source] "greaterThan x"}\\
+@{term "atLeast x"} & @{term[source] "atLeast x"}\\
+@{term "greaterThanLessThan x y"} & @{term[source] "greaterThanLessThan x y"}\\
+@{term "atLeastLessThan x y"} & @{term[source] "atLeastLessThan x y"}\\
+@{term "greaterThanAtMost x y"} & @{term[source] "greaterThanAtMost x y"}\\
+@{term "atLeastAtMost x y"} & @{term[source] "atLeastAtMost x y"}\\
+@{term[mode=xsymbols] "UN i:{..n}. A"} & @{term[source] "\<Union> i \<in> {..n}. A"}\\
+@{term[mode=xsymbols] "UN i:{..<n}. A"} & @{term[source] "\<Union> i \<in> {..<n}. A"}\\
+\multicolumn{2}{@ {}l@ {}}{Similarly for @{text"\<Inter>"} instead of @{text"\<Union>"}}\\
+@{term "setsum (%x. t) {a..b}"} & @{term[source] "setsum (\<lambda>x. t) {a..b}"}\\
+@{term "setsum (%x. t) {a..<b}"} & @{term[source] "setsum (\<lambda>x. t) {a..<b}"}\\
+@{term "setsum (%x. t) {..b}"} & @{term[source] "setsum (\<lambda>x. t) {..b}"}\\
+@{term "setsum (%x. t) {..<b}"} & @{term[source] "setsum (\<lambda>x. t) {..<b}"}\\
+\multicolumn{2}{@ {}l@ {}}{Similarly for @{text"\<Prod>"} instead of @{text"\<Sum>"}}\\
+\end{supertabular}
+
+
+\section{Power}
+
+\begin{tabular}{@ {} l @ {~::~} l @ {}}
+@{const Power.power} & @{typeof Power.power}
+\end{tabular}
+
+
+\section{Option}
+
+@{datatype option}
+\bigskip
+
+\begin{tabular}{@ {} l @ {~::~} l @ {}}
+@{const Option.the} & @{typeof Option.the}\\
+@{const Option.map} & @{typ[source]"('a \<Rightarrow> 'b) \<Rightarrow> 'a option \<Rightarrow> 'b option"}\\
+@{const Option.set} & @{term_type_only Option.set "'a option \<Rightarrow> 'a set"}\\
+@{const Option.bind} & @{term_type_only Option.bind "'a option \<Rightarrow> ('a \<Rightarrow> 'b option) \<Rightarrow> 'b option"}
+\end{tabular}
+
+\section{List}
+
+@{datatype list}
+\bigskip
+
+\begin{supertabular}{@ {} l @ {~::~} l @ {}}
+@{const List.append} & @{typeof List.append}\\
+@{const List.butlast} & @{typeof List.butlast}\\
+@{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}\\
+@{const List.length} & @{typeof List.length}\\
+@{const List.lenlex} & @{term_type_only List.lenlex "('a*'a)set\<Rightarrow>('a list * 'a list)set"}\\
+@{const List.lex} & @{term_type_only List.lex "('a*'a)set\<Rightarrow>('a list * 'a list)set"}\\
+@{const List.lexn} & @{term_type_only List.lexn "('a*'a)set\<Rightarrow>nat\<Rightarrow>('a list * 'a list)set"}\\
+@{const List.lexord} & @{term_type_only List.lexord "('a*'a)set\<Rightarrow>('a list * 'a list)set"}\\
+@{const List.listrel} & @{term_type_only List.listrel "('a*'b)set\<Rightarrow>('a list * 'b list)set"}\\
+@{const List.listrel1} & @{term_type_only List.listrel1 "('a*'a)set\<Rightarrow>('a list * 'a list)set"}\\
+@{const List.lists} & @{term_type_only List.lists "'a set\<Rightarrow>'a list set"}\\
+@{const List.listset} & @{term_type_only List.listset "'a set list \<Rightarrow> 'a list set"}\\
+@{const List.listsum} & @{typeof List.listsum}\\
+@{const List.list_all2} & @{typeof List.list_all2}\\
+@{const List.list_update} & @{typeof List.list_update}\\
+@{const List.map} & @{typeof List.map}\\
+@{const List.measures} & @{term_type_only List.measures "('a\<Rightarrow>nat)list\<Rightarrow>('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}\\
+@{const List.replicate} & @{typeof List.replicate}\\
+@{const List.rev} & @{typeof List.rev}\\
+@{const List.rotate} & @{typeof List.rotate}\\
+@{const List.rotate1} & @{typeof List.rotate1}\\
+@{const List.set} & @{term_type_only List.set "'a list \<Rightarrow> 'a set"}\\
+@{const List.sort} & @{typeof List.sort}\\
+@{const List.sorted} & @{typeof List.sorted}\\
+@{const List.splice} & @{typeof List.splice}\\
+@{const List.sublist} & @{typeof List.sublist}\\
+@{const List.take} & @{typeof List.take}\\
+@{const List.takeWhile} & @{typeof List.takeWhile}\\
+@{const List.tl} & @{typeof List.tl}\\
+@{const List.upt} & @{typeof List.upt}\\
+@{const List.upto} & @{typeof List.upto}\\
+@{const List.zip} & @{typeof List.zip}\\
+\end{supertabular}
+
+\subsubsection*{Syntax}
+
+\begin{supertabular}{@ {} l @ {\quad$\equiv$\quad} l @ {}}
+@{text"[x\<^isub>1,\<dots>,x\<^isub>n]"} & @{text"x\<^isub>1 # \<dots> # x\<^isub>n # []"}\\
+@{term"[m..<n]"} & @{term[source]"upt m n"}\\
+@{term"[i..j]"} & @{term[source]"upto i j"}\\
+@{text"[e. x \<leftarrow> xs]"} & @{term"map (%x. e) xs"}\\
+@{term"[x \<leftarrow> xs. b]"} & @{term[source]"filter (\<lambda>x. b) xs"} \\
+@{term"xs[n := x]"} & @{term[source]"list_update xs n x"}\\
+@{term"\<Sum>x\<leftarrow>xs. e"} & @{term[source]"listsum (map (\<lambda>x. e) xs)"}\\
+\end{supertabular}
+\medskip
+
+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}
+
+Maps model partial functions and are often used as finite tables. However,
+the domain of a map may be infinite.
+
+\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)"}\\
+@{const Map.dom} & @{term_type_only Map.dom "('a\<Rightarrow>'b option)\<Rightarrow>'a set"}\\
+@{const Map.ran} & @{term_type_only Map.ran "('a\<Rightarrow>'b option)\<Rightarrow>'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{supertabular}
+
+\subsubsection*{Syntax}
+
+\begin{tabular}{@ {} l @ {\quad$\equiv$\quad} l @ {}}
+@{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}
+
+*}
+(*<*)
+end
+(*>*)
\ No newline at end of file

--- a/doc-src/Main/Makefile	Mon Aug 27 21:19:16 2012 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,24 +0,0 @@
-
-## targets
-
-default: dvi
-
-
-## dependencies
-
-include ../Makefile.in
-
-NAME = main
-
-FILES = ../../lib/texinputs/isabelle.sty ../../lib/texinputs/isabellesym.sty ../pdfsetup.sty $(NAME).tex	\
-  Docs/document/Main_Doc.tex
-
-dvi: $(NAME).dvi
-
-$(NAME).dvi: $(FILES)
-	$(LATEX) $(NAME)
-
-pdf: $(NAME).pdf
-
-$(NAME).pdf: $(FILES)
-	$(PDFLATEX) $(NAME)

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Main/document/build	Mon Aug 27 21:30:18 2012 +0200
@@ -0,0 +1,11 @@
+#!/bin/bash
+
+set -e
+
+FORMAT="$1"
+VARIANT="$2"
+
+"$ISABELLE_TOOL" latex -o sty
+"$ISABELLE_TOOL" latex -o "$FORMAT"
+"$ISABELLE_TOOL" latex -o "$FORMAT"
+

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Main/document/root.tex	Mon Aug 27 21:30:18 2012 +0200
@@ -0,0 +1,38 @@
+\documentclass[12pt,a4paper]{article}
+
+\oddsidemargin=4.6mm
+\evensidemargin=4.6mm
+\textwidth=150mm
+\topmargin=4.6mm
+\headheight=0mm
+\headsep=0mm
+\textheight=234mm
+
+\usepackage{isabelle,isabellesym}
+\usepackage{amssymb}
+\usepackage[only,bigsqcap]{stmaryrd}
+
+% this should be the last package used
+\usepackage{pdfsetup}
+
+% urls in roman style, theory text in math-similar italics
+\urlstyle{rm}
+\isabellestyle{it}
+
+% for uniform font size
+\renewcommand{\isastyle}{\isastyleminor}
+
+\parindent 0pt\parskip 0.5ex
+
+\usepackage{supertabular}
+
+\begin{document}
+
+\title{What's in Main}
+\author{Tobias Nipkow}
+\date{\today}
+\maketitle
+
+\input{Main_Doc.tex}
+
+\end{document}

--- a/doc-src/Main/main.tex	Mon Aug 27 21:19:16 2012 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,42 +0,0 @@
-\documentclass[12pt,a4paper]{article}
-
-\oddsidemargin=4.6mm
-\evensidemargin=4.6mm
-\textwidth=150mm
-\topmargin=4.6mm
-\headheight=0mm
-\headsep=0mm
-\textheight=234mm
-
-\usepackage{../../lib/texinputs/isabelle,../../lib/texinputs/isabellesym}
-\usepackage{amssymb}
-\usepackage[only,bigsqcap]{stmaryrd}
-
-% this should be the last package used
-\usepackage{../pdfsetup}
-
-% urls in roman style, theory text in math-similar italics
-\urlstyle{rm}
-\isabellestyle{it}
-
-% for uniform font size
-\renewcommand{\isastyle}{\isastyleminor}
-
-\parindent 0pt\parskip 0.5ex
-
-\usepackage{supertabular}
-
-\begin{document}
-
-\title{What's in Main}
-\author{Tobias Nipkow}
-\date{\today}
-\maketitle
-
-\input{Docs/document/Main_Doc.tex}
-
-% optional bibliography
-%\bibliographystyle{abbrv}
-%\bibliography{root}
-
-\end{document}

--- a/doc-src/ROOT	Mon Aug 27 21:19:16 2012 +0200
+++ b/doc-src/ROOT	Mon Aug 27 21:30:18 2012 +0200
@@ -123,10 +123,12 @@
     "document/build"
     "document/root.tex"
 
-session Main (doc) in "Main/Docs" = HOL +
-  options [browser_info = false, document = false,
-    document_dump = document, document_dump_mode = "tex"]
+session Main (doc) in "Main" = HOL +
+  options [document_variants = "main"]
   theories Main_Doc
+  files
+    "document/build"
+    "document/root.tex"
 
 session ProgProve (doc) in "ProgProve/Thys" = HOL +
   options [browser_info = false, document = false,