# HG changeset patch
# User nipkow
# Date 1636275257 -3600
# Node ID d274100827b09729888517ee2362f77ca7baaa0d
# Parent  925b46043b843623bc1706ddb7d933bf6d5323f1
tuned page breaks

diff -r 925b46043b84 -r d274100827b0 src/Doc/Main/Main_Doc.thy
--- a/src/Doc/Main/Main_Doc.thy	Sat Nov 06 19:47:56 2021 +0100
+++ b/src/Doc/Main/Main_Doc.thy	Sun Nov 07 09:54:17 2021 +0100
@@ -91,7 +91,7 @@
 
 Available via \<^theory_text>\<open>unbundle lattice_syntax\<close>.
 
-\begin{tabular}{@ {} l @ {\quad$\equiv$\quad} l @ {}}
+\begin{supertabular}{@ {} l @ {\quad$\equiv$\quad} l @ {}}
 @{text[source]"x \<sqsubseteq> y"} & \<^term>\<open>x \<le> y\<close>\\
 @{text[source]"x \<sqsubset> y"} & \<^term>\<open>x < y\<close>\\
 @{text[source]"x \<sqinter> y"} & \<^term>\<open>inf x y\<close>\\
@@ -100,7 +100,7 @@
 @{text[source]"\<Squnion>A"} & \<^term>\<open>Sup A\<close>\\
 @{text[source]"\<top>"} & @{term[source] top}\\
 @{text[source]"\<bottom>"} & @{term[source] bot}\\
-\end{tabular}
+\end{supertabular}
 
 
 \section*{Set}
@@ -232,7 +232,7 @@
 
 \section*{Relation}
 
-\begin{tabular}{@ {} l @ {~::~} l @ {}}
+\begin{supertabular}{@ {} l @ {~::~} l @ {}}
 \<^const>\<open>Relation.converse\<close> & @{term_type_only Relation.converse "('a * 'b)set \<Rightarrow> ('b*'a)set"}\\
 \<^const>\<open>Relation.relcomp\<close> & @{term_type_only Relation.relcomp "('a*'b)set\<Rightarrow>('b*'c)set\<Rightarrow>('a*'c)set"}\\
 \<^const>\<open>Relation.Image\<close> & @{term_type_only Relation.Image "('a*'b)set\<Rightarrow>'a set\<Rightarrow>'b set"}\\
@@ -250,7 +250,7 @@
 \<^const>\<open>Relation.irrefl\<close> & @{term_type_only Relation.irrefl "('a*'a)set\<Rightarrow>bool"}\\
 \<^const>\<open>Relation.total_on\<close> & @{term_type_only Relation.total_on "'a set\<Rightarrow>('a*'a)set\<Rightarrow>bool"}\\
 \<^const>\<open>Relation.total\<close> & @{term_type_only Relation.total "('a*'a)set\<Rightarrow>bool"}\\
-\end{tabular}
+\end{supertabular}
 
 \subsubsection*{Syntax}
 
@@ -600,7 +600,7 @@
 \subsubsection*{Syntax}
 
 \begin{tabular}{@ {} l @ {\quad$\equiv$\quad} l @ {}}
-\<^term>\<open>Map.empty\<close> & \<^term>\<open>\<lambda>x. None\<close>\\
+\<^term>\<open>Map.empty\<close> & @{term[source] "\<lambda>_. None"}\\
 \<^term>\<open>m(x:=Some y)\<close> & @{term[source]"m(x:=Some y)"}\\
 \<open>m(x\<^sub>1\<mapsto>y\<^sub>1,\<dots>,x\<^sub>n\<mapsto>y\<^sub>n)\<close> & @{text[source]"m(x\<^sub>1\<mapsto>y\<^sub>1)\<dots>(x\<^sub>n\<mapsto>y\<^sub>n)"}\\
 \<open>[x\<^sub>1\<mapsto>y\<^sub>1,\<dots>,x\<^sub>n\<mapsto>y\<^sub>n]\<close> & @{text[source]"Map.empty(x\<^sub>1\<mapsto>y\<^sub>1,\<dots>,x\<^sub>n\<mapsto>y\<^sub>n)"}\\