# HG changeset patch # User wenzelm # Date 1635865285 -3600 # Node ID 4c508826fee8d66aa2fa2098a5abc0c6b680906a # Parent 9fcf80ceb863cbe84576ee319b4d38213d8f505c improve pagebreaks by *not* using supertabular too much; diff -r 9fcf80ceb863 -r 4c508826fee8 src/Doc/Main/Main_Doc.thy --- a/src/Doc/Main/Main_Doc.thy Tue Nov 02 15:40:02 2021 +0100 +++ b/src/Doc/Main/Main_Doc.thy Tue Nov 02 16:01:25 2021 +0100 @@ -35,12 +35,12 @@ \subsubsection*{Syntax} -\begin{supertabular}{@ {} l @ {\quad$\equiv$\quad} l l @ {}} +\begin{tabular}{@ {} l @ {\quad$\equiv$\quad} l l @ {}} \<^term>\\ (x = y)\ & @{term[source]"\ (x = y)"} & (\<^verbatim>\~=\)\\ @{term[source]"P \ Q"} & \<^term>\P \ Q\ \\ \<^term>\If x y z\ & @{term[source]"If x y z"}\\ \<^term>\Let e\<^sub>1 (\x. e\<^sub>2)\ & @{term[source]"Let e\<^sub>1 (\x. e\<^sub>2)"}\\ -\end{supertabular} +\end{tabular} \section*{Orderings} @@ -49,7 +49,7 @@ preorder, partial order, linear order, dense linear order and wellorder. \<^smallskip> -\begin{supertabular}{@ {} l @ {~::~} l l @ {}} +\begin{tabular}{@ {} l @ {~::~} l l @ {}} \<^const>\Orderings.less_eq\ & \<^typeof>\Orderings.less_eq\ & (\<^verbatim>\<=\)\\ \<^const>\Orderings.less\ & \<^typeof>\Orderings.less\\\ \<^const>\Orderings.Least\ & \<^typeof>\Orderings.Least\\\ @@ -60,11 +60,11 @@ @{const[source] bot} & \<^typeof>\Orderings.bot\\\ \<^const>\Orderings.mono\ & \<^typeof>\Orderings.mono\\\ \<^const>\Orderings.strict_mono\ & \<^typeof>\Orderings.strict_mono\\\ -\end{supertabular} +\end{tabular} \subsubsection*{Syntax} -\begin{supertabular}{@ {} l @ {\quad$\equiv$\quad} l l @ {}} +\begin{tabular}{@ {} l @ {\quad$\equiv$\quad} l l @ {}} @{term[source]"x \ y"} & \<^term>\x \ y\ & (\<^verbatim>\>=\)\\ @{term[source]"x > y"} & \<^term>\x > y\\\ \<^term>\\x\y. P\ & @{term[source]"\x. x \ y \ P"}\\ @@ -72,7 +72,7 @@ \multicolumn{2}{@ {}l@ {}}{Similarly for $<$, $\ge$ and $>$}\\ \<^term>\LEAST x. P\ & @{term[source]"Least (\x. P)"}\\ \<^term>\GREATEST x. P\ & @{term[source]"Greatest (\x. P)"}\\ -\end{supertabular} +\end{tabular} \section*{Lattices} @@ -91,7 +91,7 @@ Available via \<^theory_text>\unbundle lattice_syntax\. -\begin{supertabular}{@ {} l @ {\quad$\equiv$\quad} l @ {}} +\begin{tabular}{@ {} l @ {\quad$\equiv$\quad} l @ {}} @{text[source]"x \ y"} & \<^term>\x \ y\\\ @{text[source]"x \ y"} & \<^term>\x < y\\\ @{text[source]"x \ y"} & \<^term>\inf x y\\\ @@ -100,12 +100,12 @@ @{text[source]"\A"} & \<^term>\Sup A\\\ @{text[source]"\"} & @{term[source] top}\\ @{text[source]"\"} & @{term[source] bot}\\ -\end{supertabular} +\end{tabular} \section*{Set} -\begin{supertabular}{@ {} l @ {~::~} l l @ {}} +\begin{tabular}{@ {} l @ {~::~} l l @ {}} \<^const>\Set.empty\ & @{term_type_only "Set.empty" "'a set"}\\ \<^const>\Set.insert\ & @{term_type_only insert "'a\'a set\'a set"}\\ \<^const>\Collect\ & @{term_type_only Collect "('a\bool)\'a set"}\\ @@ -119,11 +119,11 @@ \<^const>\image\ & @{term_type_only image "('a\'b)\'a set\'b set"}\\ \<^const>\Ball\ & @{term_type_only Ball "'a set\('a\bool)\bool"}\\ \<^const>\Bex\ & @{term_type_only Bex "'a set\('a\bool)\bool"}\\ -\end{supertabular} +\end{tabular} \subsubsection*{Syntax} -\begin{supertabular}{@ {} l @ {\quad$\equiv$\quad} l l @ {}} +\begin{tabular}{@ {} l @ {\quad$\equiv$\quad} l l @ {}} \{a\<^sub>1,\,a\<^sub>n}\ & \insert a\<^sub>1 (\ (insert a\<^sub>n {})\)\\\ \<^term>\a \ A\ & @{term[source]"\(x \ A)"}\\ \<^term>\A \ B\ & @{term[source]"A \ B"}\\ @@ -139,12 +139,12 @@ \<^term>\\x\A. P\ & @{term[source]"Ball A (\x. P)"}\\ \<^term>\\x\A. P\ & @{term[source]"Bex A (\x. P)"}\\ \<^term>\range f\ & @{term[source]"f ` UNIV"}\\ -\end{supertabular} +\end{tabular} \section*{Fun} -\begin{supertabular}{@ {} l @ {~::~} l l @ {}} +\begin{tabular}{@ {} 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\'b)\'a set\bool"}\\ @@ -153,7 +153,7 @@ \<^const>\Fun.bij\ & \<^typeof>\Fun.bij\\\ \<^const>\Fun.bij_betw\ & @{term_type_only Fun.bij_betw "('a\'b)\'a set\'b set\bool"}\\ \<^const>\Fun.fun_upd\ & \<^typeof>\Fun.fun_upd\\\ -\end{supertabular} +\end{tabular} \subsubsection*{Syntax} @@ -206,7 +206,7 @@ Types \<^typ>\unit\ and \\\. -\begin{supertabular}{@ {} l @ {~::~} l @ {}} +\begin{tabular}{@ {} l @ {~::~} l @ {}} \<^const>\Product_Type.Unity\ & \<^typeof>\Product_Type.Unity\\\ \<^const>\Pair\ & \<^typeof>\Pair\\\ \<^const>\fst\ & \<^typeof>\fst\\\ @@ -214,7 +214,7 @@ \<^const>\case_prod\ & \<^typeof>\case_prod\\\ \<^const>\curry\ & \<^typeof>\curry\\\ \<^const>\Product_Type.Sigma\ & @{term_type_only Product_Type.Sigma "'a set\('a\'b set)\('a*'b)set"}\\ -\end{supertabular} +\end{tabular} \subsubsection*{Syntax} @@ -264,13 +264,13 @@ \section*{Equiv\_Relations} -\begin{supertabular}{@ {} l @ {~::~} l @ {}} +\begin{tabular}{@ {} l @ {~::~} l @ {}} \<^const>\Equiv_Relations.equiv\ & @{term_type_only Equiv_Relations.equiv "'a set \ ('a*'a)set\bool"}\\ \<^const>\Equiv_Relations.quotient\ & @{term_type_only Equiv_Relations.quotient "'a set \ ('a \ 'a) set \ 'a set set"}\\ \<^const>\Equiv_Relations.congruent\ & @{term_type_only Equiv_Relations.congruent "('a*'a)set\('a\'b)\bool"}\\ \<^const>\Equiv_Relations.congruent2\ & @{term_type_only Equiv_Relations.congruent2 "('a*'a)set\('b*'b)set\('a\'b\'c)\bool"}\\ %@ {const Equiv_Relations.} & @ {term_type_only Equiv_Relations. ""}\\ -\end{supertabular} +\end{tabular} \subsubsection*{Syntax} @@ -305,7 +305,7 @@ structures from semigroups up to fields. Everything is done in terms of overloaded operators: -\begin{supertabular}{@ {} l @ {~::~} l l @ {}} +\begin{tabular}{@ {} l @ {~::~} l l @ {}} \0\ & \<^typeof>\zero\\\ \1\ & \<^typeof>\one\\\ \<^const>\plus\ & \<^typeof>\plus\\\ @@ -319,7 +319,7 @@ \<^const>\Rings.dvd\ & \<^typeof>\Rings.dvd\\\ \<^const>\divide\ & \<^typeof>\divide\\\ \<^const>\modulo\ & \<^typeof>\modulo\\\ -\end{supertabular} +\end{tabular} \subsubsection*{Syntax} @@ -394,53 +394,53 @@ \section*{Finite\_Set} -\begin{supertabular}{@ {} l @ {~::~} l @ {}} +\begin{tabular}{@ {} l @ {~::~} l @ {}} \<^const>\Finite_Set.finite\ & @{term_type_only Finite_Set.finite "'a set\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 \ 'b \ 'b) \ 'b \ 'a set \ 'b"}\\ -\end{supertabular} +\end{tabular} \section*{Lattices\_Big} -\begin{supertabular}{@ {} l @ {~::~} l l @ {}} +\begin{tabular}{@ {} l @ {~::~} l l @ {}} \<^const>\Lattices_Big.Min\ & \<^typeof>\Lattices_Big.Min\\\ \<^const>\Lattices_Big.Max\ & \<^typeof>\Lattices_Big.Max\\\ \<^const>\Lattices_Big.arg_min\ & \<^typeof>\Lattices_Big.arg_min\\\ \<^const>\Lattices_Big.is_arg_min\ & \<^typeof>\Lattices_Big.is_arg_min\\\ \<^const>\Lattices_Big.arg_max\ & \<^typeof>\Lattices_Big.arg_max\\\ \<^const>\Lattices_Big.is_arg_max\ & \<^typeof>\Lattices_Big.is_arg_max\\\ -\end{supertabular} +\end{tabular} \subsubsection*{Syntax} -\begin{supertabular}{@ {} l @ {\quad$\equiv$\quad} l l @ {}} +\begin{tabular}{@ {} l @ {\quad$\equiv$\quad} l l @ {}} \<^term>\ARG_MIN f x. P\ & @{term[source]"arg_min f (\x. P)"}\\ \<^term>\ARG_MAX f x. P\ & @{term[source]"arg_max f (\x. P)"}\\ -\end{supertabular} +\end{tabular} \section*{Groups\_Big} -\begin{supertabular}{@ {} l @ {~::~} l @ {}} +\begin{tabular}{@ {} l @ {~::~} l @ {}} \<^const>\Groups_Big.sum\ & @{term_type_only Groups_Big.sum "('a \ 'b) \ 'a set \ 'b::comm_monoid_add"}\\ \<^const>\Groups_Big.prod\ & @{term_type_only Groups_Big.prod "('a \ 'b) \ 'a set \ 'b::comm_monoid_mult"}\\ -\end{supertabular} +\end{tabular} \subsubsection*{Syntax} -\begin{supertabular}{@ {} l @ {\quad$\equiv$\quad} l l @ {}} +\begin{tabular}{@ {} l @ {\quad$\equiv$\quad} l l @ {}} \<^term>\sum (\x. x) A\ & @{term[source]"sum (\x. x) A"} & (\<^verbatim>\SUM\)\\ \<^term>\sum (\x. t) A\ & @{term[source]"sum (\x. t) A"}\\ @{term[source] "\x|P. t"} & \<^term>\\x|P. t\\\ \multicolumn{2}{@ {}l@ {}}{Similarly for \\\ instead of \\\} & (\<^verbatim>\PROD\)\\ -\end{supertabular} +\end{tabular} \section*{Wellfounded} -\begin{supertabular}{@ {} l @ {~::~} l @ {}} +\begin{tabular}{@ {} l @ {~::~} l @ {}} \<^const>\Wellfounded.wf\ & @{term_type_only Wellfounded.wf "('a*'a)set\bool"}\\ \<^const>\Wellfounded.acc\ & @{term_type_only Wellfounded.acc "('a*'a)set\'a set"}\\ \<^const>\Wellfounded.measure\ & @{term_type_only Wellfounded.measure "('a\nat)\('a*'a)set"}\\ @@ -448,12 +448,12 @@ \<^const>\Wellfounded.mlex_prod\ & @{term_type_only Wellfounded.mlex_prod "('a\nat)\('a*'a)set\('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} +\end{tabular} \section*{Set\_Interval} % \<^theory>\HOL.Set_Interval\ -\begin{supertabular}{@ {} l @ {~::~} l @ {}} +\begin{tabular}{@ {} l @ {~::~} l @ {}} \<^const>\lessThan\ & @{term_type_only lessThan "'a::ord \ 'a set"}\\ \<^const>\atMost\ & @{term_type_only atMost "'a::ord \ 'a set"}\\ \<^const>\greaterThan\ & @{term_type_only greaterThan "'a::ord \ 'a set"}\\ @@ -462,11 +462,11 @@ \<^const>\atLeastLessThan\ & @{term_type_only atLeastLessThan "'a::ord \ 'a \ 'a set"}\\ \<^const>\greaterThanAtMost\ & @{term_type_only greaterThanAtMost "'a::ord \ 'a \ 'a set"}\\ \<^const>\atLeastAtMost\ & @{term_type_only atLeastAtMost "'a::ord \ 'a \ 'a set"}\\ -\end{supertabular} +\end{tabular} \subsubsection*{Syntax} -\begin{supertabular}{@ {} l @ {\quad$\equiv$\quad} l @ {}} +\begin{tabular}{@ {} 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"}\\ @@ -483,7 +483,7 @@ \<^term>\sum (\x. t) {..b}\ & @{term[source] "sum (\x. t) {..b}"}\\ \<^term>\sum (\x. t) {.. & @{term[source] "sum (\x. t) {..\\ instead of \\\}\\ -\end{supertabular} +\end{tabular} \section*{Power} @@ -564,13 +564,13 @@ \subsubsection*{Syntax} -\begin{supertabular}{@ {} l @ {\quad$\equiv$\quad} l @ {}} +\begin{tabular}{@ {} l @ {\quad$\equiv$\quad} l @ {}} \[x\<^sub>1,\,x\<^sub>n]\ & \x\<^sub>1 # \ # x\<^sub>n # []\\\ \<^term>\[m.. & @{term[source]"upt m n"}\\ \<^term>\[i..j]\ & @{term[source]"upto i j"}\\ \<^term>\xs[n := x]\ & @{term[source]"list_update xs n x"}\\ \<^term>\\x\xs. e\ & @{term[source]"listsum (map (\x. e) xs)"}\\ -\end{supertabular} +\end{tabular} \<^medskip> Filter input syntax \[pat \ e. b]\, where @@ -585,7 +585,7 @@ Maps model partial functions and are often used as finite tables. However, the domain of a map may be infinite. -\begin{supertabular}{@ {} l @ {~::~} l @ {}} +\begin{tabular}{@ {} l @ {~::~} l @ {}} \<^const>\Map.empty\ & \<^typeof>\Map.empty\\\ \<^const>\Map.map_add\ & \<^typeof>\Map.map_add\\\ \<^const>\Map.map_comp\ & \<^typeof>\Map.map_comp\\\ @@ -595,7 +595,7 @@ \<^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} +\end{tabular} \subsubsection*{Syntax}