# HG changeset patch
# User blanchet
# Date 1459159547 -7200
# Node ID b751a43c500159e83fc800e93cfa5c88721db969
# Parent  8745b8079b97fa06478b18b0cc4c08871115469e
tuning

diff -r 8745b8079b97 -r b751a43c5001 CONTRIBUTORS
--- a/CONTRIBUTORS	Mon Mar 28 12:05:47 2016 +0200
+++ b/CONTRIBUTORS	Mon Mar 28 12:05:47 2016 +0200
@@ -21,8 +21,8 @@
 -----------------------------
 
 * Winter 2016: Jasmin Blanchette, Inria & LORIA & MPII, Aymeric Bouzy,
-  Ecole polytechnique, Andreas Lochbihler, ETH Zurich, and Dmitriy Traytel,
-  ETH Zurich
+  Ecole polytechnique, Andreas Lochbihler, ETH Zurich, Andrei Popescu,
+  Middlesex University, and Dmitriy Traytel, ETH Zurich
   'corec' command and friends.
 
 * Winter 2016: Manuel Eberl, TUM
diff -r 8745b8079b97 -r b751a43c5001 src/Doc/Datatypes/Datatypes.thy
--- a/src/Doc/Datatypes/Datatypes.thy	Mon Mar 28 12:05:47 2016 +0200
+++ b/src/Doc/Datatypes/Datatypes.thy	Mon Mar 28 12:05:47 2016 +0200
@@ -19,8 +19,8 @@
   "~~/src/HOL/Library/Simps_Case_Conv"
 begin
 
-section \<open> Introduction
-  \label{sec:introduction} \<close>
+section \<open>Introduction
+  \label{sec:introduction}\<close>
 
 text \<open>
 The 2013 edition of Isabelle introduced a definitional package for freely
@@ -147,16 +147,16 @@
 \<close>
 
 
-section \<open> Defining Datatypes
-  \label{sec:defining-datatypes} \<close>
+section \<open>Defining Datatypes
+  \label{sec:defining-datatypes}\<close>
 
 text \<open>
 Datatypes can be specified using the @{command datatype} command.
 \<close>
 
 
-subsection \<open> Introductory Examples
-  \label{ssec:datatype-introductory-examples} \<close>
+subsection \<open>Introductory Examples
+  \label{ssec:datatype-introductory-examples}\<close>
 
 text \<open>
 Datatypes are illustrated through concrete examples featuring different flavors
@@ -165,8 +165,8 @@
 \<close>
 
 
-subsubsection \<open> Nonrecursive Types
-  \label{sssec:datatype-nonrecursive-types} \<close>
+subsubsection \<open>Nonrecursive Types
+  \label{sssec:datatype-nonrecursive-types}\<close>
 
 text \<open>
 Datatypes are introduced by specifying the desired names and argument types for
@@ -217,8 +217,8 @@
 \<close>
 
 
-subsubsection \<open> Simple Recursion
-  \label{sssec:datatype-simple-recursion} \<close>
+subsubsection \<open>Simple Recursion
+  \label{sssec:datatype-simple-recursion}\<close>
 
 text \<open>
 Natural numbers are the simplest example of a recursive type:
@@ -235,8 +235,8 @@
     datatype (*<*)(in early) (*>*)('a, 'b) tlist = TNil 'b | TCons 'a "('a, 'b) tlist"
 
 
-subsubsection \<open> Mutual Recursion
-  \label{sssec:datatype-mutual-recursion} \<close>
+subsubsection \<open>Mutual Recursion
+  \label{sssec:datatype-mutual-recursion}\<close>
 
 text \<open>
 \emph{Mutually recursive} types are introduced simultaneously and may refer to
@@ -261,8 +261,8 @@
       Const 'a | Var 'b | Expr "('a, 'b) exp"
 
 
-subsubsection \<open> Nested Recursion
-  \label{sssec:datatype-nested-recursion} \<close>
+subsubsection \<open>Nested Recursion
+  \label{sssec:datatype-nested-recursion}\<close>
 
 text \<open>
 \emph{Nested recursion} occurs when recursive occurrences of a type appear under
@@ -336,8 +336,8 @@
 \<close>
 
 
-subsubsection \<open> Auxiliary Constants
-  \label{sssec:datatype-auxiliary-constants} \<close>
+subsubsection \<open>Auxiliary Constants
+  \label{sssec:datatype-auxiliary-constants}\<close>
 
 text \<open>
 The @{command datatype} command introduces various constants in addition to
@@ -432,7 +432,7 @@
 (*>*)
     datatype ('a, 'b) prod (infixr "*" 20) = Pair 'a 'b
 
-text \<open> \blankline \<close>
+text \<open>\blankline\<close>
 
     datatype (set: 'a) list =
       null: Nil ("[]")
@@ -449,18 +449,18 @@
 
     syntax "_list" :: "args \<Rightarrow> 'a list" ("[(_)]")
 
-text \<open> \blankline \<close>
+text \<open>\blankline\<close>
 
     translations
       "[x, xs]" == "x # [xs]"
       "[x]" == "x # []"
 
 
-subsection \<open> Command Syntax
-  \label{ssec:datatype-command-syntax} \<close>
-
-subsubsection \<open> \keyw{datatype}
-  \label{sssec:datatype-new} \<close>
+subsection \<open>Command Syntax
+  \label{ssec:datatype-command-syntax}\<close>
+
+subsubsection \<open>\keyw{datatype}
+  \label{sssec:datatype-new}\<close>
 
 text \<open>
 \begin{matharray}{rcl}
@@ -570,8 +570,8 @@
 \<close>
 
 
-subsubsection \<open> \keyw{datatype_compat}
-  \label{sssec:datatype-compat} \<close>
+subsubsection \<open>\keyw{datatype_compat}
+  \label{sssec:datatype-compat}\<close>
 
 text \<open>
 \begin{matharray}{rcl}
@@ -591,9 +591,9 @@
 
     datatype_compat even_nat odd_nat
 
-text \<open> \blankline \<close>
-
-    ML \<open> Old_Datatype_Data.get_info @{theory} @{type_name even_nat} \<close>
+text \<open>\blankline\<close>
+
+    ML \<open>Old_Datatype_Data.get_info @{theory} @{type_name even_nat}\<close>
 
 text \<open>
 The syntactic entity \synt{name} denotes an identifier @{cite "isabelle-isar-ref"}.
@@ -620,8 +620,8 @@
 \<close>
 
 
-subsection \<open> Generated Constants
-  \label{ssec:datatype-generated-constants} \<close>
+subsection \<open>Generated Constants
+  \label{ssec:datatype-generated-constants}\<close>
 
 text \<open>
 Given a datatype @{text "('a\<^sub>1, \<dots>, 'a\<^sub>m) t"} with $m$ live type variables
@@ -663,8 +663,8 @@
 \<close>
 
 
-subsection \<open> Generated Theorems
-  \label{ssec:datatype-generated-theorems} \<close>
+subsection \<open>Generated Theorems
+  \label{ssec:datatype-generated-theorems}\<close>
 
 text \<open>
 The characteristic theorems generated by @{command datatype} are grouped in
@@ -706,8 +706,8 @@
 \<close>
 
 
-subsubsection \<open> Free Constructor Theorems
-  \label{sssec:free-constructor-theorems} \<close>
+subsubsection \<open>Free Constructor Theorems
+  \label{sssec:free-constructor-theorems}\<close>
 
 (*<*)
     consts nonnull :: 'a
@@ -850,8 +850,8 @@
 \<close>
 
 
-subsubsection \<open> Functorial Theorems
-  \label{sssec:functorial-theorems} \<close>
+subsubsection \<open>Functorial Theorems
+  \label{sssec:functorial-theorems}\<close>
 
 text \<open>
 The functorial theorems are generated for type constructors with at least
@@ -1082,8 +1082,8 @@
 \<close>
 
 
-subsubsection \<open> Inductive Theorems
-  \label{sssec:inductive-theorems} \<close>
+subsubsection \<open>Inductive Theorems
+  \label{sssec:inductive-theorems}\<close>
 
 text \<open>
 The inductive theorems are as follows:
@@ -1135,11 +1135,11 @@
 \<close>
 
 
-subsection \<open> Proof Method
-  \label{ssec:datatype-proof-method} \<close>
-
-subsubsection \<open> \textit{countable_datatype}
-  \label{sssec:datatype-compat} \<close>
+subsection \<open>Proof Method
+  \label{ssec:datatype-proof-method}\<close>
+
+subsubsection \<open>\textit{countable_datatype}
+  \label{sssec:datatype-compat}\<close>
 
 text \<open>
 The theory @{file "~~/src/HOL/Library/Countable.thy"} provides a
@@ -1152,8 +1152,8 @@
       by countable_datatype
 
 
-subsection \<open> Compatibility Issues
-  \label{ssec:datatype-compatibility-issues} \<close>
+subsection \<open>Compatibility Issues
+  \label{ssec:datatype-compatibility-issues}\<close>
 
 text \<open>
 The command @{command datatype} has been designed to be highly compatible with
@@ -1233,8 +1233,8 @@
 \<close>
 
 
-section \<open> Defining Primitively Recursive Functions
-  \label{sec:defining-primitively-recursive-functions} \<close>
+section \<open>Defining Primitively Recursive Functions
+  \label{sec:defining-primitively-recursive-functions}\<close>
 
 text \<open>
 Recursive functions over datatypes can be specified using the @{command primrec}
@@ -1245,8 +1245,8 @@
 \<close>
 
 
-subsection \<open> Introductory Examples
-  \label{ssec:primrec-introductory-examples} \<close>
+subsection \<open>Introductory Examples
+  \label{ssec:primrec-introductory-examples}\<close>
 
 text \<open>
 Primitive recursion is illustrated through concrete examples based on the
@@ -1255,8 +1255,8 @@
 \<close>
 
 
-subsubsection \<open> Nonrecursive Types
-  \label{sssec:primrec-nonrecursive-types} \<close>
+subsubsection \<open>Nonrecursive Types
+  \label{sssec:primrec-nonrecursive-types}\<close>
 
 text \<open>
 Primitive recursion removes one layer of constructors on the left-hand side in
@@ -1267,19 +1267,19 @@
       "bool_of_trool Faalse \<longleftrightarrow> False"
     | "bool_of_trool Truue \<longleftrightarrow> True"
 
-text \<open> \blankline \<close>
+text \<open>\blankline\<close>
 
     primrec the_list :: "'a option \<Rightarrow> 'a list" where
       "the_list None = []"
     | "the_list (Some a) = [a]"
 
-text \<open> \blankline \<close>
+text \<open>\blankline\<close>
 
     primrec the_default :: "'a \<Rightarrow> 'a option \<Rightarrow> 'a" where
       "the_default d None = d"
     | "the_default _ (Some a) = a"
 
-text \<open> \blankline \<close>
+text \<open>\blankline\<close>
 
     primrec mirrror :: "('a, 'b, 'c) triple \<Rightarrow> ('c, 'b, 'a) triple" where
       "mirrror (Triple a b c) = Triple c b a"
@@ -1293,8 +1293,8 @@
 \<close>
 
 
-subsubsection \<open> Simple Recursion
-  \label{sssec:primrec-simple-recursion} \<close>
+subsubsection \<open>Simple Recursion
+  \label{sssec:primrec-simple-recursion}\<close>
 
 text \<open>
 For simple recursive types, recursive calls on a constructor argument are
@@ -1305,7 +1305,7 @@
       "replicate Zero _ = []"
     | "replicate (Succ n) x = x # replicate n x"
 
-text \<open> \blankline \<close>
+text \<open>\blankline\<close>
 
     primrec (nonexhaustive) at :: "'a list \<Rightarrow> nat \<Rightarrow> 'a" where
       "at (x # xs) j =
@@ -1313,7 +1313,7 @@
             Zero \<Rightarrow> x
           | Succ j' \<Rightarrow> at xs j')"
 
-text \<open> \blankline \<close>
+text \<open>\blankline\<close>
 
     primrec (*<*)(in early) (transfer) (*>*)tfold :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> ('a, 'b) tlist \<Rightarrow> 'b" where
       "tfold _ (TNil y) = y"
@@ -1344,8 +1344,8 @@
     | "at_least_two _ \<longleftrightarrow> False"
 
 
-subsubsection \<open> Mutual Recursion
-  \label{sssec:primrec-mutual-recursion} \<close>
+subsubsection \<open>Mutual Recursion
+  \label{sssec:primrec-mutual-recursion}\<close>
 
 text \<open>
 The syntax for mutually recursive functions over mutually recursive datatypes
@@ -1360,7 +1360,7 @@
     | "nat_of_even_nat (Even_Succ n) = Succ (nat_of_odd_nat n)"
     | "nat_of_odd_nat (Odd_Succ n) = Succ (nat_of_even_nat n)"
 
-text \<open> \blankline \<close>
+text \<open>\blankline\<close>
 
     primrec
       eval\<^sub>e :: "('a \<Rightarrow> int) \<Rightarrow> ('b \<Rightarrow> int) \<Rightarrow> ('a, 'b) exp \<Rightarrow> int" and
@@ -1390,8 +1390,8 @@
     | "odd (Succ n) = even n"
 
 
-subsubsection \<open> Nested Recursion
-  \label{sssec:primrec-nested-recursion} \<close>
+subsubsection \<open>Nested Recursion
+  \label{sssec:primrec-nested-recursion}\<close>
 
 text \<open>
 In a departure from the old datatype package, nested recursion is normally
@@ -1442,7 +1442,7 @@
       "relabel_ft f (FTLeaf x) = FTLeaf (f x)"
     | "relabel_ft f (FTNode g) = FTNode (\<lambda>x. relabel_ft f (g x))"
 
-text \<open> \blankline \<close>
+text \<open>\blankline\<close>
 
     primrec (nonexhaustive) subtree_ft :: "'a \<Rightarrow> 'a ftree \<Rightarrow> 'a ftree" where
       "subtree_ft x (FTNode g) = g x"
@@ -1456,19 +1456,19 @@
 
     datatype 'a ftree2 = FTLeaf2 'a | FTNode2 "'a \<Rightarrow> 'a \<Rightarrow> 'a ftree2"
 
-text \<open> \blankline \<close>
+text \<open>\blankline\<close>
 
     primrec (*<*)(in early) (*>*)relabel_ft2 :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a ftree2 \<Rightarrow> 'a ftree2" where
       "relabel_ft2 f (FTLeaf2 x) = FTLeaf2 (f x)"
     | "relabel_ft2 f (FTNode2 g) = FTNode2 (op \<circ> (op \<circ> (relabel_ft2 f)) g)"
 
-text \<open> \blankline \<close>
+text \<open>\blankline\<close>
 
     primrec relabel_ft2 :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a ftree2 \<Rightarrow> 'a ftree2" where
       "relabel_ft2 f (FTLeaf2 x) = FTLeaf2 (f x)"
     | "relabel_ft2 f (FTNode2 g) = FTNode2 (\<lambda>x y. relabel_ft2 f (g x y))"
 
-text \<open> \blankline \<close>
+text \<open>\blankline\<close>
 
     primrec (nonexhaustive) subtree_ft2 :: "'a \<Rightarrow> 'a \<Rightarrow> 'a ftree2 \<Rightarrow> 'a ftree2" where
       "subtree_ft2 x y (FTNode2 g) = g x y"
@@ -1483,8 +1483,8 @@
        n \<ge> m \<and> list_all (increasing_tree (n + 1)) ts"
 
 
-subsubsection \<open> Nested-as-Mutual Recursion
-  \label{sssec:primrec-nested-as-mutual-recursion} \<close>
+subsubsection \<open>Nested-as-Mutual Recursion
+  \label{sssec:primrec-nested-as-mutual-recursion}\<close>
 
 (*<*)
     locale n2m
@@ -1565,11 +1565,11 @@
 (*>*)
 
 
-subsection \<open> Command Syntax
-  \label{ssec:primrec-command-syntax} \<close>
-
-subsubsection \<open> \keyw{primrec}
-  \label{sssec:primrec-new} \<close>
+subsection \<open>Command Syntax
+  \label{ssec:primrec-command-syntax}\<close>
+
+subsubsection \<open>\keyw{primrec}
+  \label{sssec:primrec-new}\<close>
 
 text \<open>
 \begin{matharray}{rcl}
@@ -1622,8 +1622,8 @@
 \<close>
 
 
-subsection \<open> Generated Theorems
-  \label{ssec:primrec-generated-theorems} \<close>
+subsection \<open>Generated Theorems
+  \label{ssec:primrec-generated-theorems}\<close>
 
 (*<*)
     context early
@@ -1668,8 +1668,8 @@
 (*>*)
 
 
-subsection \<open> Recursive Default Values for Selectors
-  \label{ssec:primrec-recursive-default-values-for-selectors} \<close>
+subsection \<open>Recursive Default Values for Selectors
+  \label{ssec:primrec-recursive-default-values-for-selectors}\<close>
 
 text \<open>
 A datatype selector @{text un_D} can have a default value for each constructor
@@ -1712,7 +1712,7 @@
 (*>*)
     consts termi\<^sub>0 :: 'a
 
-text \<open> \blankline \<close>
+text \<open>\blankline\<close>
 
     datatype ('a, 'b) tlist =
       TNil (termi: 'b)
@@ -1721,7 +1721,7 @@
       "ttl (TNil y) = TNil y"
     | "termi (TCons _ xs) = termi\<^sub>0 xs"
 
-text \<open> \blankline \<close>
+text \<open>\blankline\<close>
 
     overloading
       termi\<^sub>0 \<equiv> "termi\<^sub>0 :: ('a, 'b) tlist \<Rightarrow> 'b"
@@ -1731,14 +1731,14 @@
     | "termi\<^sub>0 (TCons x xs) = termi\<^sub>0 xs"
     end
 
-text \<open> \blankline \<close>
+text \<open>\blankline\<close>
 
     lemma termi_TCons[simp]: "termi (TCons x xs) = termi xs"
       by (cases xs) auto
 
 
-subsection \<open> Compatibility Issues
-  \label{ssec:primrec-compatibility-issues} \<close>
+subsection \<open>Compatibility Issues
+  \label{ssec:primrec-compatibility-issues}\<close>
 
 text \<open>
 The command @{command primrec}'s behavior on new-style datatypes has been
@@ -1757,8 +1757,8 @@
 \<close>
 
 
-section \<open> Defining Codatatypes
-  \label{sec:defining-codatatypes} \<close>
+section \<open>Defining Codatatypes
+  \label{sec:defining-codatatypes}\<close>
 
 text \<open>
 Codatatypes can be specified using the @{command codatatype} command. The
@@ -1770,11 +1770,11 @@
 \<close>
 
 
-subsection \<open> Introductory Examples
-  \label{ssec:codatatype-introductory-examples} \<close>
-
-subsubsection \<open> Simple Corecursion
-  \label{sssec:codatatype-simple-corecursion} \<close>
+subsection \<open>Introductory Examples
+  \label{ssec:codatatype-introductory-examples}\<close>
+
+subsubsection \<open>Simple Corecursion
+  \label{sssec:codatatype-simple-corecursion}\<close>
 
 text \<open>
 Non-corecursive codatatypes coincide with the corresponding datatypes, so they
@@ -1836,8 +1836,8 @@
 \<close>
 
 
-subsubsection \<open> Mutual Corecursion
-  \label{sssec:codatatype-mutual-corecursion} \<close>
+subsubsection \<open>Mutual Corecursion
+  \label{sssec:codatatype-mutual-corecursion}\<close>
 
 text \<open>
 \noindent
@@ -1848,8 +1848,8 @@
     and odd_enat = Odd_ESucc even_enat
 
 
-subsubsection \<open> Nested Corecursion
-  \label{sssec:codatatype-nested-corecursion} \<close>
+subsubsection \<open>Nested Corecursion
+  \label{sssec:codatatype-nested-corecursion}\<close>
 
 text \<open>
 \noindent
@@ -1858,20 +1858,20 @@
 
     codatatype 'a tree\<^sub>i\<^sub>i = Node\<^sub>i\<^sub>i (lbl\<^sub>i\<^sub>i: 'a) (sub\<^sub>i\<^sub>i: "'a tree\<^sub>i\<^sub>i llist")
 
-text \<open> \blankline \<close>
+text \<open>\blankline\<close>
 
     codatatype 'a tree\<^sub>i\<^sub>s = Node\<^sub>i\<^sub>s (lbl\<^sub>i\<^sub>s: 'a) (sub\<^sub>i\<^sub>s: "'a tree\<^sub>i\<^sub>s fset")
 
-text \<open> \blankline \<close>
+text \<open>\blankline\<close>
 
     codatatype 'a sm = SM (accept: bool) (trans: "'a \<Rightarrow> 'a sm")
 
 
-subsection \<open> Command Syntax
-  \label{ssec:codatatype-command-syntax} \<close>
-
-subsubsection \<open> \keyw{codatatype}
-  \label{sssec:codatatype} \<close>
+subsection \<open>Command Syntax
+  \label{ssec:codatatype-command-syntax}\<close>
+
+subsubsection \<open>\keyw{codatatype}
+  \label{sssec:codatatype}\<close>
 
 text \<open>
 \begin{matharray}{rcl}
@@ -1892,8 +1892,8 @@
 \<close>
 
 
-subsection \<open> Generated Constants
-  \label{ssec:codatatype-generated-constants} \<close>
+subsection \<open>Generated Constants
+  \label{ssec:codatatype-generated-constants}\<close>
 
 text \<open>
 Given a codatatype @{text "('a\<^sub>1, \<dots>, 'a\<^sub>m) t"}
@@ -1911,8 +1911,8 @@
 \<close>
 
 
-subsection \<open> Generated Theorems
-  \label{ssec:codatatype-generated-theorems} \<close>
+subsection \<open>Generated Theorems
+  \label{ssec:codatatype-generated-theorems}\<close>
 
 text \<open>
 The characteristic theorems generated by @{command codatatype} are grouped in
@@ -1938,8 +1938,8 @@
 \<close>
 
 
-subsubsection \<open> Coinductive Theorems
-  \label{sssec:coinductive-theorems} \<close>
+subsubsection \<open>Coinductive Theorems
+  \label{sssec:coinductive-theorems}\<close>
 
 text \<open>
 The coinductive theorems are listed below for @{typ "'a llist"}:
@@ -2030,8 +2030,8 @@
 \<close>
 
 
-section \<open> Defining Primitively Corecursive Functions
-  \label{sec:defining-primitively-corecursive-functions} \<close>
+section \<open>Defining Primitively Corecursive Functions
+  \label{sec:defining-primitively-corecursive-functions}\<close>
 
 text \<open>
 Corecursive functions can be specified using the @{command primcorec} and
@@ -2079,8 +2079,8 @@
 \<close>
 
 
-subsection \<open> Introductory Examples
-  \label{ssec:primcorec-introductory-examples} \<close>
+subsection \<open>Introductory Examples
+  \label{ssec:primcorec-introductory-examples}\<close>
 
 text \<open>
 Primitive corecursion is illustrated through concrete examples based on the
@@ -2092,8 +2092,8 @@
 \<close>
 
 
-subsubsection \<open> Simple Corecursion
-  \label{sssec:primcorec-simple-corecursion} \<close>
+subsubsection \<open>Simple Corecursion
+  \label{sssec:primcorec-simple-corecursion}\<close>
 
 text \<open>
 Following the code view, corecursive calls are allowed on the right-hand side as
@@ -2104,7 +2104,7 @@
     primcorec (*<*)(transfer) (*>*)literate :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a llist" where
       "literate g x = LCons x (literate g (g x))"
 
-text \<open> \blankline \<close>
+text \<open>\blankline\<close>
 
     primcorec siterate :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a stream" where
       "siterate g x = SCons x (siterate g (g x))"
@@ -2201,8 +2201,8 @@
 \<close>
 
 
-subsubsection \<open> Mutual Corecursion
-  \label{sssec:primcorec-mutual-corecursion} \<close>
+subsubsection \<open>Mutual Corecursion
+  \label{sssec:primcorec-mutual-corecursion}\<close>
 
 text \<open>
 The syntax for mutually corecursive functions over mutually corecursive
@@ -2217,8 +2217,8 @@
     | "odd_infty = Odd_ESucc even_infty"
 
 
-subsubsection \<open> Nested Corecursion
-  \label{sssec:primcorec-nested-corecursion} \<close>
+subsubsection \<open>Nested Corecursion
+  \label{sssec:primcorec-nested-corecursion}\<close>
 
 text \<open>
 The next pair of examples generalize the @{const literate} and @{const siterate}
@@ -2231,7 +2231,7 @@
     primcorec iterate\<^sub>i\<^sub>i :: "('a \<Rightarrow> 'a llist) \<Rightarrow> 'a \<Rightarrow> 'a tree\<^sub>i\<^sub>i" where
       "iterate\<^sub>i\<^sub>i g x = Node\<^sub>i\<^sub>i x (lmap (iterate\<^sub>i\<^sub>i g) (g x))"
 
-text \<open> \blankline \<close>
+text \<open>\blankline\<close>
 
     primcorec iterate\<^sub>i\<^sub>s :: "('a \<Rightarrow> 'a fset) \<Rightarrow> 'a \<Rightarrow> 'a tree\<^sub>i\<^sub>s" where
       "iterate\<^sub>i\<^sub>s g x = Node\<^sub>i\<^sub>s x (fimage (iterate\<^sub>i\<^sub>s g) (g x))"
@@ -2285,17 +2285,17 @@
     primcorec sm_of_dfa :: "('q \<Rightarrow> 'a \<Rightarrow> 'q) \<Rightarrow> 'q set \<Rightarrow> 'q \<Rightarrow> 'a sm" where
       "sm_of_dfa \<delta> F q = SM (q \<in> F) (\<lambda>a. sm_of_dfa \<delta> F (\<delta> q a))"
 
-text \<open> \blankline \<close>
+text \<open>\blankline\<close>
 
     primcorec empty_sm :: "'a sm" where
       "empty_sm = SM False (\<lambda>_. empty_sm)"
 
-text \<open> \blankline \<close>
+text \<open>\blankline\<close>
 
     primcorec not_sm :: "'a sm \<Rightarrow> 'a sm" where
       "not_sm M = SM (\<not> accept M) (\<lambda>a. not_sm (trans M a))"
 
-text \<open> \blankline \<close>
+text \<open>\blankline\<close>
 
     primcorec or_sm :: "'a sm \<Rightarrow> 'a sm \<Rightarrow> 'a sm" where
       "or_sm M N =
@@ -2311,14 +2311,14 @@
     codatatype ('a, 'b) sm2 =
       SM2 (accept2: bool) (trans2: "'a \<Rightarrow> 'b \<Rightarrow> ('a, 'b) sm2")
 
-text \<open> \blankline \<close>
+text \<open>\blankline\<close>
 
     primcorec
       (*<*)(in early) (*>*)sm2_of_dfa :: "('q \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'q) \<Rightarrow> 'q set \<Rightarrow> 'q \<Rightarrow> ('a, 'b) sm2"
     where
       "sm2_of_dfa \<delta> F q = SM2 (q \<in> F) (op \<circ> (op \<circ> (sm2_of_dfa \<delta> F)) (\<delta> q))"
 
-text \<open> \blankline \<close>
+text \<open>\blankline\<close>
 
     primcorec
       sm2_of_dfa :: "('q \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'q) \<Rightarrow> 'q set \<Rightarrow> 'q \<Rightarrow> ('a, 'b) sm2"
@@ -2326,8 +2326,8 @@
       "sm2_of_dfa \<delta> F q = SM2 (q \<in> F) (\<lambda>a b. sm2_of_dfa \<delta> F (\<delta> q a b))"
 
 
-subsubsection \<open> Nested-as-Mutual Corecursion
-  \label{sssec:primcorec-nested-as-mutual-corecursion} \<close>
+subsubsection \<open>Nested-as-Mutual Corecursion
+  \label{sssec:primcorec-nested-as-mutual-corecursion}\<close>
 
 text \<open>
 Just as it is possible to recurse over nested recursive datatypes as if they
@@ -2366,8 +2366,8 @@
 (*>*)
 
 
-subsubsection \<open> Constructor View
-  \label{ssec:primrec-constructor-view} \<close>
+subsubsection \<open>Constructor View
+  \label{ssec:primrec-constructor-view}\<close>
 
 (*<*)
     locale ctr_view
@@ -2437,8 +2437,8 @@
 \<close>
 
 
-subsubsection \<open> Destructor View
-  \label{ssec:primrec-destructor-view} \<close>
+subsubsection \<open>Destructor View
+  \label{ssec:primrec-destructor-view}\<close>
 
 (*<*)
     locale dtr_view
@@ -2457,13 +2457,13 @@
     | "lhd (literate _ x) = x"
     | "ltl (literate g x) = literate g (g x)"
 
-text \<open> \blankline \<close>
+text \<open>\blankline\<close>
 
     primcorec siterate :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a stream" where
       "shd (siterate _ x) = x"
     | "stl (siterate g x) = siterate g (g x)"
 
-text \<open> \blankline \<close>
+text \<open>\blankline\<close>
 
     primcorec every_snd :: "'a stream \<Rightarrow> 'a stream" where
       "shd (every_snd s) = shd s"
@@ -2544,7 +2544,7 @@
     | "un_Even_ESucc even_infty = odd_infty"
     | "un_Odd_ESucc odd_infty = even_infty"
 
-text \<open> \blankline \<close>
+text \<open>\blankline\<close>
 
     primcorec iterate\<^sub>i\<^sub>i :: "('a \<Rightarrow> 'a llist) \<Rightarrow> 'a \<Rightarrow> 'a tree\<^sub>i\<^sub>i" where
       "lbl\<^sub>i\<^sub>i (iterate\<^sub>i\<^sub>i g x) = x"
@@ -2554,11 +2554,11 @@
 (*>*)
 
 
-subsection \<open> Command Syntax
-  \label{ssec:primcorec-command-syntax} \<close>
-
-subsubsection \<open> \keyw{primcorec} and \keyw{primcorecursive}
-  \label{sssec:primcorecursive-and-primcorec} \<close>
+subsection \<open>Command Syntax
+  \label{ssec:primcorec-command-syntax}\<close>
+
+subsubsection \<open>\keyw{primcorec} and \keyw{primcorecursive}
+  \label{sssec:primcorecursive-and-primcorec}\<close>
 
 text \<open>
 \begin{matharray}{rcl}
@@ -2621,8 +2621,8 @@
 \<close>
 
 
-subsection \<open> Generated Theorems
-  \label{ssec:primcorec-generated-theorems} \<close>
+subsection \<open>Generated Theorems
+  \label{ssec:primcorec-generated-theorems}\<close>
 
 text \<open>
 The @{command primcorec} and @{command primcorecursive} commands generate the
@@ -2719,8 +2719,8 @@
 
 
 (*
-subsection \<open> Recursive Default Values for Selectors
-  \label{ssec:primcorec-recursive-default-values-for-selectors} \<close>
+subsection \<open>Recursive Default Values for Selectors
+  \label{ssec:primcorec-recursive-default-values-for-selectors}\<close>
 
 text \<open>
 partial_function to the rescue
@@ -2728,8 +2728,8 @@
 *)
 
 
-section \<open> Registering Bounded Natural Functors
-  \label{sec:registering-bounded-natural-functors} \<close>
+section \<open>Registering Bounded Natural Functors
+  \label{sec:registering-bounded-natural-functors}\<close>
 
 text \<open>
 The (co)datatype package can be set up to allow nested recursion through
@@ -2739,8 +2739,8 @@
 \<close>
 
 
-subsection \<open> Bounded Natural Functors
-  \label{ssec:bounded-natural-functors} \<close>
+subsection \<open>Bounded Natural Functors
+  \label{ssec:bounded-natural-functors}\<close>
 
 text \<open>
 Bounded natural functors (BNFs) are a semantic criterion for where
@@ -2773,8 +2773,8 @@
 \<close>
 
 
-subsection \<open> Introductory Examples
-  \label{ssec:bnf-introductory-examples} \<close>
+subsection \<open>Introductory Examples
+  \label{ssec:bnf-introductory-examples}\<close>
 
 text \<open>
 The example below shows how to register a type as a BNF using the @{command bnf}
@@ -2789,16 +2789,16 @@
     typedef ('d, 'a) fn = "UNIV :: ('d \<Rightarrow> 'a) set"
       by simp
 
-text \<open> \blankline \<close>
+text \<open>\blankline\<close>
 
     setup_lifting type_definition_fn
 
-text \<open> \blankline \<close>
+text \<open>\blankline\<close>
 
     lift_definition map_fn :: "('a \<Rightarrow> 'b) \<Rightarrow> ('d, 'a) fn \<Rightarrow> ('d, 'b) fn" is "op \<circ>" .
     lift_definition set_fn :: "('d, 'a) fn \<Rightarrow> 'a set" is range .
 
-text \<open> \blankline \<close>
+text \<open>\blankline\<close>
 
     lift_definition
       pred_fn :: "('a \<Rightarrow> bool) \<Rightarrow> ('d, 'a) fn \<Rightarrow> bool"
@@ -2810,7 +2810,7 @@
     is
       "rel_fun (op =)" .
 
-text \<open> \blankline \<close>
+text \<open>\blankline\<close>
 
     bnf "('d, 'a) fn"
       map: map_fn
@@ -2866,7 +2866,7 @@
         unfolding fun_eq_iff by transfer simp
     qed
 
-text \<open> \blankline \<close>
+text \<open>\blankline\<close>
 
     print_theorems
     print_bnfs
@@ -2925,7 +2925,7 @@
       xval :: 'a
       yval :: 'a
 
-text \<open> \blankline \<close>
+text \<open>\blankline\<close>
 
     copy_bnf ('a, 'z) point_ext
 
@@ -2970,17 +2970,17 @@
     bnf_axiomatization (setA: 'a, setB: 'b, setC: 'c) F
       [wits: "'a \<Rightarrow> ('a, 'b, 'c) F"]
 
-text \<open> \blankline \<close>
+text \<open>\blankline\<close>
 
     print_theorems
     print_bnfs
 
 
-subsection \<open> Command Syntax
-  \label{ssec:bnf-command-syntax} \<close>
-
-subsubsection \<open> \keyw{bnf}
-  \label{sssec:bnf} \<close>
+subsection \<open>Command Syntax
+  \label{ssec:bnf-command-syntax}\<close>
+
+subsubsection \<open>\keyw{bnf}
+  \label{sssec:bnf}\<close>
 
 text \<open>
 \begin{matharray}{rcl}
@@ -3012,8 +3012,8 @@
 %%% TODO: elaborate on proof obligations
 \<close>
 
-subsubsection \<open> \keyw{lift_bnf}
-  \label{sssec:lift-bnf} \<close>
+subsubsection \<open>\keyw{lift_bnf}
+  \label{sssec:lift-bnf}\<close>
 
 text \<open>
 \begin{matharray}{rcl}
@@ -3048,8 +3048,8 @@
 specifying the @{text no_warn_wits} option.
 \<close>
 
-subsubsection \<open> \keyw{copy_bnf}
-  \label{sssec:copy-bnf} \<close>
+subsubsection \<open>\keyw{copy_bnf}
+  \label{sssec:copy-bnf}\<close>
 
 text \<open>
 \begin{matharray}{rcl}
@@ -3069,8 +3069,8 @@
 nonemptiness witnesses.
 \<close>
 
-subsubsection \<open> \keyw{bnf_axiomatization}
-  \label{sssec:bnf-axiomatization} \<close>
+subsubsection \<open>\keyw{bnf_axiomatization}
+  \label{sssec:bnf-axiomatization}\<close>
 
 text \<open>
 \begin{matharray}{rcl}
@@ -3114,8 +3114,8 @@
 \<close>
 
 
-subsubsection \<open> \keyw{print_bnfs}
-  \label{sssec:print-bnfs} \<close>
+subsubsection \<open>\keyw{print_bnfs}
+  \label{sssec:print-bnfs}\<close>
 
 text \<open>
 \begin{matharray}{rcl}
@@ -3128,8 +3128,8 @@
 \<close>
 
 
-section \<open> Deriving Destructors and Theorems for Free Constructors
-  \label{sec:deriving-destructors-and-theorems-for-free-constructors} \<close>
+section \<open>Deriving Destructors and Theorems for Free Constructors
+  \label{sec:deriving-destructors-and-theorems-for-free-constructors}\<close>
 
 text \<open>
 The derivation of convenience theorems for types equipped with free constructors,
@@ -3146,16 +3146,16 @@
 
 
 (*
-subsection \<open> Introductory Example
-  \label{ssec:ctors-introductory-example} \<close>
+subsection \<open>Introductory Example
+  \label{ssec:ctors-introductory-example}\<close>
 *)
 
 
-subsection \<open> Command Syntax
-  \label{ssec:ctors-command-syntax} \<close>
-
-subsubsection \<open> \keyw{free_constructors}
-  \label{sssec:free-constructors} \<close>
+subsection \<open>Command Syntax
+  \label{ssec:ctors-command-syntax}\<close>
+
+subsubsection \<open>\keyw{free_constructors}
+  \label{sssec:free-constructors}\<close>
 
 text \<open>
 \begin{matharray}{rcl}
@@ -3195,8 +3195,8 @@
 \<close>
 
 
-subsubsection \<open> \keyw{simps_of_case}
-  \label{sssec:simps-of-case} \<close>
+subsubsection \<open>\keyw{simps_of_case}
+  \label{sssec:simps-of-case}\<close>
 
 text \<open>
 \begin{matharray}{rcl}
@@ -3234,8 +3234,8 @@
 \<close>
 
 
-subsubsection \<open> \keyw{case_of_simps}
-  \label{sssec:case-of-simps} \<close>
+subsubsection \<open>\keyw{case_of_simps}
+  \label{sssec:case-of-simps}\<close>
 
 text \<open>
 \begin{matharray}{rcl}
@@ -3275,8 +3275,8 @@
 
 
 (*
-section \<open> Using the Standard ML Interface
-  \label{sec:using-the-standard-ml-interface} \<close>
+section \<open>Using the Standard ML Interface
+  \label{sec:using-the-standard-ml-interface}\<close>
 
 text \<open>
 The package's programmatic interface.
@@ -3284,8 +3284,8 @@
 *)
 
 
-section \<open> Selecting Plugins
-  \label{sec:selecting-plugins} \<close>
+section \<open>Selecting Plugins
+  \label{sec:selecting-plugins}\<close>
 
 text \<open>
 Plugins extend the (co)datatype package to interoperate with other Isabelle
@@ -3305,8 +3305,8 @@
 @{cite "sternagel-thiemann-2015"}.
 \<close>
 
-subsection \<open> Code Generator
-  \label{ssec:code-generator} \<close>
+subsection \<open>Code Generator
+  \label{ssec:code-generator}\<close>
 
 text \<open>
 The \hthm{code} plugin registers freely generated types, including
@@ -3342,8 +3342,8 @@
 \<close>
 
 
-subsection \<open> Size
-  \label{ssec:size} \<close>
+subsection \<open>Size
+  \label{ssec:size}\<close>
 
 text \<open>
 For each datatype @{text t}, the \hthm{size} plugin generates a generic size
@@ -3392,8 +3392,8 @@
 \<close>
 
 
-subsection \<open> Transfer
-  \label{ssec:transfer} \<close>
+subsection \<open>Transfer
+  \label{ssec:transfer}\<close>
 
 text \<open>
 For each (co)datatype with live type arguments and each manually registered BNF,
@@ -3451,8 +3451,8 @@
 \<close>
 
 
-subsection \<open> Lifting
-  \label{ssec:lifting} \<close>
+subsection \<open>Lifting
+  \label{ssec:lifting}\<close>
 
 text \<open>
 For each (co)datatype and each manually registered BNF with at least one live
@@ -3477,8 +3477,8 @@
 \<close>
 
 
-subsection \<open> Quickcheck
-  \label{ssec:quickcheck} \<close>
+subsection \<open>Quickcheck
+  \label{ssec:quickcheck}\<close>
 
 text \<open>
 The integration of datatypes with Quickcheck is accomplished by the
@@ -3496,8 +3496,8 @@
 \<close>
 
 
-subsection \<open> Program Extraction
-  \label{ssec:program-extraction} \<close>
+subsection \<open>Program Extraction
+  \label{ssec:program-extraction}\<close>
 
 text \<open>
 The \hthm{extraction} plugin provides realizers for induction and case analysis,
@@ -3507,13 +3507,12 @@
 \<close>
 
 
-section \<open> Known Bugs and Limitations
-  \label{sec:known-bugs-and-limitations} \<close>
+section \<open>Known Bugs and Limitations
+  \label{sec:known-bugs-and-limitations}\<close>
 
 text \<open>
-This section lists the known bugs and limitations in the (co)datatype package at
-the time of this writing. Many of them are expected to be addressed in future
-releases.
+This section lists the known bugs and limitations of the (co)datatype package at
+the time of this writing.
 
 \begin{enumerate}
 \setlength{\itemsep}{0pt}