tuning
authorblanchet
Mon Mar 28 12:05:47 2016 +0200 (2016-03-28)
changeset 62731b751a43c5001
parent 62730 8745b8079b97
child 62732 bf31fd0231ba
tuning
CONTRIBUTORS
src/Doc/Datatypes/Datatypes.thy
     1.1 --- a/CONTRIBUTORS	Mon Mar 28 12:05:47 2016 +0200
     1.2 +++ b/CONTRIBUTORS	Mon Mar 28 12:05:47 2016 +0200
     1.3 @@ -21,8 +21,8 @@
     1.4  -----------------------------
     1.5  
     1.6  * Winter 2016: Jasmin Blanchette, Inria & LORIA & MPII, Aymeric Bouzy,
     1.7 -  Ecole polytechnique, Andreas Lochbihler, ETH Zurich, and Dmitriy Traytel,
     1.8 -  ETH Zurich
     1.9 +  Ecole polytechnique, Andreas Lochbihler, ETH Zurich, Andrei Popescu,
    1.10 +  Middlesex University, and Dmitriy Traytel, ETH Zurich
    1.11    'corec' command and friends.
    1.12  
    1.13  * Winter 2016: Manuel Eberl, TUM
     2.1 --- a/src/Doc/Datatypes/Datatypes.thy	Mon Mar 28 12:05:47 2016 +0200
     2.2 +++ b/src/Doc/Datatypes/Datatypes.thy	Mon Mar 28 12:05:47 2016 +0200
     2.3 @@ -19,8 +19,8 @@
     2.4    "~~/src/HOL/Library/Simps_Case_Conv"
     2.5  begin
     2.6  
     2.7 -section \<open> Introduction
     2.8 -  \label{sec:introduction} \<close>
     2.9 +section \<open>Introduction
    2.10 +  \label{sec:introduction}\<close>
    2.11  
    2.12  text \<open>
    2.13  The 2013 edition of Isabelle introduced a definitional package for freely
    2.14 @@ -147,16 +147,16 @@
    2.15  \<close>
    2.16  
    2.17  
    2.18 -section \<open> Defining Datatypes
    2.19 -  \label{sec:defining-datatypes} \<close>
    2.20 +section \<open>Defining Datatypes
    2.21 +  \label{sec:defining-datatypes}\<close>
    2.22  
    2.23  text \<open>
    2.24  Datatypes can be specified using the @{command datatype} command.
    2.25  \<close>
    2.26  
    2.27  
    2.28 -subsection \<open> Introductory Examples
    2.29 -  \label{ssec:datatype-introductory-examples} \<close>
    2.30 +subsection \<open>Introductory Examples
    2.31 +  \label{ssec:datatype-introductory-examples}\<close>
    2.32  
    2.33  text \<open>
    2.34  Datatypes are illustrated through concrete examples featuring different flavors
    2.35 @@ -165,8 +165,8 @@
    2.36  \<close>
    2.37  
    2.38  
    2.39 -subsubsection \<open> Nonrecursive Types
    2.40 -  \label{sssec:datatype-nonrecursive-types} \<close>
    2.41 +subsubsection \<open>Nonrecursive Types
    2.42 +  \label{sssec:datatype-nonrecursive-types}\<close>
    2.43  
    2.44  text \<open>
    2.45  Datatypes are introduced by specifying the desired names and argument types for
    2.46 @@ -217,8 +217,8 @@
    2.47  \<close>
    2.48  
    2.49  
    2.50 -subsubsection \<open> Simple Recursion
    2.51 -  \label{sssec:datatype-simple-recursion} \<close>
    2.52 +subsubsection \<open>Simple Recursion
    2.53 +  \label{sssec:datatype-simple-recursion}\<close>
    2.54  
    2.55  text \<open>
    2.56  Natural numbers are the simplest example of a recursive type:
    2.57 @@ -235,8 +235,8 @@
    2.58      datatype (*<*)(in early) (*>*)('a, 'b) tlist = TNil 'b | TCons 'a "('a, 'b) tlist"
    2.59  
    2.60  
    2.61 -subsubsection \<open> Mutual Recursion
    2.62 -  \label{sssec:datatype-mutual-recursion} \<close>
    2.63 +subsubsection \<open>Mutual Recursion
    2.64 +  \label{sssec:datatype-mutual-recursion}\<close>
    2.65  
    2.66  text \<open>
    2.67  \emph{Mutually recursive} types are introduced simultaneously and may refer to
    2.68 @@ -261,8 +261,8 @@
    2.69        Const 'a | Var 'b | Expr "('a, 'b) exp"
    2.70  
    2.71  
    2.72 -subsubsection \<open> Nested Recursion
    2.73 -  \label{sssec:datatype-nested-recursion} \<close>
    2.74 +subsubsection \<open>Nested Recursion
    2.75 +  \label{sssec:datatype-nested-recursion}\<close>
    2.76  
    2.77  text \<open>
    2.78  \emph{Nested recursion} occurs when recursive occurrences of a type appear under
    2.79 @@ -336,8 +336,8 @@
    2.80  \<close>
    2.81  
    2.82  
    2.83 -subsubsection \<open> Auxiliary Constants
    2.84 -  \label{sssec:datatype-auxiliary-constants} \<close>
    2.85 +subsubsection \<open>Auxiliary Constants
    2.86 +  \label{sssec:datatype-auxiliary-constants}\<close>
    2.87  
    2.88  text \<open>
    2.89  The @{command datatype} command introduces various constants in addition to
    2.90 @@ -432,7 +432,7 @@
    2.91  (*>*)
    2.92      datatype ('a, 'b) prod (infixr "*" 20) = Pair 'a 'b
    2.93  
    2.94 -text \<open> \blankline \<close>
    2.95 +text \<open>\blankline\<close>
    2.96  
    2.97      datatype (set: 'a) list =
    2.98        null: Nil ("[]")
    2.99 @@ -449,18 +449,18 @@
   2.100  
   2.101      syntax "_list" :: "args \<Rightarrow> 'a list" ("[(_)]")
   2.102  
   2.103 -text \<open> \blankline \<close>
   2.104 +text \<open>\blankline\<close>
   2.105  
   2.106      translations
   2.107        "[x, xs]" == "x # [xs]"
   2.108        "[x]" == "x # []"
   2.109  
   2.110  
   2.111 -subsection \<open> Command Syntax
   2.112 -  \label{ssec:datatype-command-syntax} \<close>
   2.113 -
   2.114 -subsubsection \<open> \keyw{datatype}
   2.115 -  \label{sssec:datatype-new} \<close>
   2.116 +subsection \<open>Command Syntax
   2.117 +  \label{ssec:datatype-command-syntax}\<close>
   2.118 +
   2.119 +subsubsection \<open>\keyw{datatype}
   2.120 +  \label{sssec:datatype-new}\<close>
   2.121  
   2.122  text \<open>
   2.123  \begin{matharray}{rcl}
   2.124 @@ -570,8 +570,8 @@
   2.125  \<close>
   2.126  
   2.127  
   2.128 -subsubsection \<open> \keyw{datatype_compat}
   2.129 -  \label{sssec:datatype-compat} \<close>
   2.130 +subsubsection \<open>\keyw{datatype_compat}
   2.131 +  \label{sssec:datatype-compat}\<close>
   2.132  
   2.133  text \<open>
   2.134  \begin{matharray}{rcl}
   2.135 @@ -591,9 +591,9 @@
   2.136  
   2.137      datatype_compat even_nat odd_nat
   2.138  
   2.139 -text \<open> \blankline \<close>
   2.140 -
   2.141 -    ML \<open> Old_Datatype_Data.get_info @{theory} @{type_name even_nat} \<close>
   2.142 +text \<open>\blankline\<close>
   2.143 +
   2.144 +    ML \<open>Old_Datatype_Data.get_info @{theory} @{type_name even_nat}\<close>
   2.145  
   2.146  text \<open>
   2.147  The syntactic entity \synt{name} denotes an identifier @{cite "isabelle-isar-ref"}.
   2.148 @@ -620,8 +620,8 @@
   2.149  \<close>
   2.150  
   2.151  
   2.152 -subsection \<open> Generated Constants
   2.153 -  \label{ssec:datatype-generated-constants} \<close>
   2.154 +subsection \<open>Generated Constants
   2.155 +  \label{ssec:datatype-generated-constants}\<close>
   2.156  
   2.157  text \<open>
   2.158  Given a datatype @{text "('a\<^sub>1, \<dots>, 'a\<^sub>m) t"} with $m$ live type variables
   2.159 @@ -663,8 +663,8 @@
   2.160  \<close>
   2.161  
   2.162  
   2.163 -subsection \<open> Generated Theorems
   2.164 -  \label{ssec:datatype-generated-theorems} \<close>
   2.165 +subsection \<open>Generated Theorems
   2.166 +  \label{ssec:datatype-generated-theorems}\<close>
   2.167  
   2.168  text \<open>
   2.169  The characteristic theorems generated by @{command datatype} are grouped in
   2.170 @@ -706,8 +706,8 @@
   2.171  \<close>
   2.172  
   2.173  
   2.174 -subsubsection \<open> Free Constructor Theorems
   2.175 -  \label{sssec:free-constructor-theorems} \<close>
   2.176 +subsubsection \<open>Free Constructor Theorems
   2.177 +  \label{sssec:free-constructor-theorems}\<close>
   2.178  
   2.179  (*<*)
   2.180      consts nonnull :: 'a
   2.181 @@ -850,8 +850,8 @@
   2.182  \<close>
   2.183  
   2.184  
   2.185 -subsubsection \<open> Functorial Theorems
   2.186 -  \label{sssec:functorial-theorems} \<close>
   2.187 +subsubsection \<open>Functorial Theorems
   2.188 +  \label{sssec:functorial-theorems}\<close>
   2.189  
   2.190  text \<open>
   2.191  The functorial theorems are generated for type constructors with at least
   2.192 @@ -1082,8 +1082,8 @@
   2.193  \<close>
   2.194  
   2.195  
   2.196 -subsubsection \<open> Inductive Theorems
   2.197 -  \label{sssec:inductive-theorems} \<close>
   2.198 +subsubsection \<open>Inductive Theorems
   2.199 +  \label{sssec:inductive-theorems}\<close>
   2.200  
   2.201  text \<open>
   2.202  The inductive theorems are as follows:
   2.203 @@ -1135,11 +1135,11 @@
   2.204  \<close>
   2.205  
   2.206  
   2.207 -subsection \<open> Proof Method
   2.208 -  \label{ssec:datatype-proof-method} \<close>
   2.209 -
   2.210 -subsubsection \<open> \textit{countable_datatype}
   2.211 -  \label{sssec:datatype-compat} \<close>
   2.212 +subsection \<open>Proof Method
   2.213 +  \label{ssec:datatype-proof-method}\<close>
   2.214 +
   2.215 +subsubsection \<open>\textit{countable_datatype}
   2.216 +  \label{sssec:datatype-compat}\<close>
   2.217  
   2.218  text \<open>
   2.219  The theory @{file "~~/src/HOL/Library/Countable.thy"} provides a
   2.220 @@ -1152,8 +1152,8 @@
   2.221        by countable_datatype
   2.222  
   2.223  
   2.224 -subsection \<open> Compatibility Issues
   2.225 -  \label{ssec:datatype-compatibility-issues} \<close>
   2.226 +subsection \<open>Compatibility Issues
   2.227 +  \label{ssec:datatype-compatibility-issues}\<close>
   2.228  
   2.229  text \<open>
   2.230  The command @{command datatype} has been designed to be highly compatible with
   2.231 @@ -1233,8 +1233,8 @@
   2.232  \<close>
   2.233  
   2.234  
   2.235 -section \<open> Defining Primitively Recursive Functions
   2.236 -  \label{sec:defining-primitively-recursive-functions} \<close>
   2.237 +section \<open>Defining Primitively Recursive Functions
   2.238 +  \label{sec:defining-primitively-recursive-functions}\<close>
   2.239  
   2.240  text \<open>
   2.241  Recursive functions over datatypes can be specified using the @{command primrec}
   2.242 @@ -1245,8 +1245,8 @@
   2.243  \<close>
   2.244  
   2.245  
   2.246 -subsection \<open> Introductory Examples
   2.247 -  \label{ssec:primrec-introductory-examples} \<close>
   2.248 +subsection \<open>Introductory Examples
   2.249 +  \label{ssec:primrec-introductory-examples}\<close>
   2.250  
   2.251  text \<open>
   2.252  Primitive recursion is illustrated through concrete examples based on the
   2.253 @@ -1255,8 +1255,8 @@
   2.254  \<close>
   2.255  
   2.256  
   2.257 -subsubsection \<open> Nonrecursive Types
   2.258 -  \label{sssec:primrec-nonrecursive-types} \<close>
   2.259 +subsubsection \<open>Nonrecursive Types
   2.260 +  \label{sssec:primrec-nonrecursive-types}\<close>
   2.261  
   2.262  text \<open>
   2.263  Primitive recursion removes one layer of constructors on the left-hand side in
   2.264 @@ -1267,19 +1267,19 @@
   2.265        "bool_of_trool Faalse \<longleftrightarrow> False"
   2.266      | "bool_of_trool Truue \<longleftrightarrow> True"
   2.267  
   2.268 -text \<open> \blankline \<close>
   2.269 +text \<open>\blankline\<close>
   2.270  
   2.271      primrec the_list :: "'a option \<Rightarrow> 'a list" where
   2.272        "the_list None = []"
   2.273      | "the_list (Some a) = [a]"
   2.274  
   2.275 -text \<open> \blankline \<close>
   2.276 +text \<open>\blankline\<close>
   2.277  
   2.278      primrec the_default :: "'a \<Rightarrow> 'a option \<Rightarrow> 'a" where
   2.279        "the_default d None = d"
   2.280      | "the_default _ (Some a) = a"
   2.281  
   2.282 -text \<open> \blankline \<close>
   2.283 +text \<open>\blankline\<close>
   2.284  
   2.285      primrec mirrror :: "('a, 'b, 'c) triple \<Rightarrow> ('c, 'b, 'a) triple" where
   2.286        "mirrror (Triple a b c) = Triple c b a"
   2.287 @@ -1293,8 +1293,8 @@
   2.288  \<close>
   2.289  
   2.290  
   2.291 -subsubsection \<open> Simple Recursion
   2.292 -  \label{sssec:primrec-simple-recursion} \<close>
   2.293 +subsubsection \<open>Simple Recursion
   2.294 +  \label{sssec:primrec-simple-recursion}\<close>
   2.295  
   2.296  text \<open>
   2.297  For simple recursive types, recursive calls on a constructor argument are
   2.298 @@ -1305,7 +1305,7 @@
   2.299        "replicate Zero _ = []"
   2.300      | "replicate (Succ n) x = x # replicate n x"
   2.301  
   2.302 -text \<open> \blankline \<close>
   2.303 +text \<open>\blankline\<close>
   2.304  
   2.305      primrec (nonexhaustive) at :: "'a list \<Rightarrow> nat \<Rightarrow> 'a" where
   2.306        "at (x # xs) j =
   2.307 @@ -1313,7 +1313,7 @@
   2.308              Zero \<Rightarrow> x
   2.309            | Succ j' \<Rightarrow> at xs j')"
   2.310  
   2.311 -text \<open> \blankline \<close>
   2.312 +text \<open>\blankline\<close>
   2.313  
   2.314      primrec (*<*)(in early) (transfer) (*>*)tfold :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> ('a, 'b) tlist \<Rightarrow> 'b" where
   2.315        "tfold _ (TNil y) = y"
   2.316 @@ -1344,8 +1344,8 @@
   2.317      | "at_least_two _ \<longleftrightarrow> False"
   2.318  
   2.319  
   2.320 -subsubsection \<open> Mutual Recursion
   2.321 -  \label{sssec:primrec-mutual-recursion} \<close>
   2.322 +subsubsection \<open>Mutual Recursion
   2.323 +  \label{sssec:primrec-mutual-recursion}\<close>
   2.324  
   2.325  text \<open>
   2.326  The syntax for mutually recursive functions over mutually recursive datatypes
   2.327 @@ -1360,7 +1360,7 @@
   2.328      | "nat_of_even_nat (Even_Succ n) = Succ (nat_of_odd_nat n)"
   2.329      | "nat_of_odd_nat (Odd_Succ n) = Succ (nat_of_even_nat n)"
   2.330  
   2.331 -text \<open> \blankline \<close>
   2.332 +text \<open>\blankline\<close>
   2.333  
   2.334      primrec
   2.335        eval\<^sub>e :: "('a \<Rightarrow> int) \<Rightarrow> ('b \<Rightarrow> int) \<Rightarrow> ('a, 'b) exp \<Rightarrow> int" and
   2.336 @@ -1390,8 +1390,8 @@
   2.337      | "odd (Succ n) = even n"
   2.338  
   2.339  
   2.340 -subsubsection \<open> Nested Recursion
   2.341 -  \label{sssec:primrec-nested-recursion} \<close>
   2.342 +subsubsection \<open>Nested Recursion
   2.343 +  \label{sssec:primrec-nested-recursion}\<close>
   2.344  
   2.345  text \<open>
   2.346  In a departure from the old datatype package, nested recursion is normally
   2.347 @@ -1442,7 +1442,7 @@
   2.348        "relabel_ft f (FTLeaf x) = FTLeaf (f x)"
   2.349      | "relabel_ft f (FTNode g) = FTNode (\<lambda>x. relabel_ft f (g x))"
   2.350  
   2.351 -text \<open> \blankline \<close>
   2.352 +text \<open>\blankline\<close>
   2.353  
   2.354      primrec (nonexhaustive) subtree_ft :: "'a \<Rightarrow> 'a ftree \<Rightarrow> 'a ftree" where
   2.355        "subtree_ft x (FTNode g) = g x"
   2.356 @@ -1456,19 +1456,19 @@
   2.357  
   2.358      datatype 'a ftree2 = FTLeaf2 'a | FTNode2 "'a \<Rightarrow> 'a \<Rightarrow> 'a ftree2"
   2.359  
   2.360 -text \<open> \blankline \<close>
   2.361 +text \<open>\blankline\<close>
   2.362  
   2.363      primrec (*<*)(in early) (*>*)relabel_ft2 :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a ftree2 \<Rightarrow> 'a ftree2" where
   2.364        "relabel_ft2 f (FTLeaf2 x) = FTLeaf2 (f x)"
   2.365      | "relabel_ft2 f (FTNode2 g) = FTNode2 (op \<circ> (op \<circ> (relabel_ft2 f)) g)"
   2.366  
   2.367 -text \<open> \blankline \<close>
   2.368 +text \<open>\blankline\<close>
   2.369  
   2.370      primrec relabel_ft2 :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a ftree2 \<Rightarrow> 'a ftree2" where
   2.371        "relabel_ft2 f (FTLeaf2 x) = FTLeaf2 (f x)"
   2.372      | "relabel_ft2 f (FTNode2 g) = FTNode2 (\<lambda>x y. relabel_ft2 f (g x y))"
   2.373  
   2.374 -text \<open> \blankline \<close>
   2.375 +text \<open>\blankline\<close>
   2.376  
   2.377      primrec (nonexhaustive) subtree_ft2 :: "'a \<Rightarrow> 'a \<Rightarrow> 'a ftree2 \<Rightarrow> 'a ftree2" where
   2.378        "subtree_ft2 x y (FTNode2 g) = g x y"
   2.379 @@ -1483,8 +1483,8 @@
   2.380         n \<ge> m \<and> list_all (increasing_tree (n + 1)) ts"
   2.381  
   2.382  
   2.383 -subsubsection \<open> Nested-as-Mutual Recursion
   2.384 -  \label{sssec:primrec-nested-as-mutual-recursion} \<close>
   2.385 +subsubsection \<open>Nested-as-Mutual Recursion
   2.386 +  \label{sssec:primrec-nested-as-mutual-recursion}\<close>
   2.387  
   2.388  (*<*)
   2.389      locale n2m
   2.390 @@ -1565,11 +1565,11 @@
   2.391  (*>*)
   2.392  
   2.393  
   2.394 -subsection \<open> Command Syntax
   2.395 -  \label{ssec:primrec-command-syntax} \<close>
   2.396 -
   2.397 -subsubsection \<open> \keyw{primrec}
   2.398 -  \label{sssec:primrec-new} \<close>
   2.399 +subsection \<open>Command Syntax
   2.400 +  \label{ssec:primrec-command-syntax}\<close>
   2.401 +
   2.402 +subsubsection \<open>\keyw{primrec}
   2.403 +  \label{sssec:primrec-new}\<close>
   2.404  
   2.405  text \<open>
   2.406  \begin{matharray}{rcl}
   2.407 @@ -1622,8 +1622,8 @@
   2.408  \<close>
   2.409  
   2.410  
   2.411 -subsection \<open> Generated Theorems
   2.412 -  \label{ssec:primrec-generated-theorems} \<close>
   2.413 +subsection \<open>Generated Theorems
   2.414 +  \label{ssec:primrec-generated-theorems}\<close>
   2.415  
   2.416  (*<*)
   2.417      context early
   2.418 @@ -1668,8 +1668,8 @@
   2.419  (*>*)
   2.420  
   2.421  
   2.422 -subsection \<open> Recursive Default Values for Selectors
   2.423 -  \label{ssec:primrec-recursive-default-values-for-selectors} \<close>
   2.424 +subsection \<open>Recursive Default Values for Selectors
   2.425 +  \label{ssec:primrec-recursive-default-values-for-selectors}\<close>
   2.426  
   2.427  text \<open>
   2.428  A datatype selector @{text un_D} can have a default value for each constructor
   2.429 @@ -1712,7 +1712,7 @@
   2.430  (*>*)
   2.431      consts termi\<^sub>0 :: 'a
   2.432  
   2.433 -text \<open> \blankline \<close>
   2.434 +text \<open>\blankline\<close>
   2.435  
   2.436      datatype ('a, 'b) tlist =
   2.437        TNil (termi: 'b)
   2.438 @@ -1721,7 +1721,7 @@
   2.439        "ttl (TNil y) = TNil y"
   2.440      | "termi (TCons _ xs) = termi\<^sub>0 xs"
   2.441  
   2.442 -text \<open> \blankline \<close>
   2.443 +text \<open>\blankline\<close>
   2.444  
   2.445      overloading
   2.446        termi\<^sub>0 \<equiv> "termi\<^sub>0 :: ('a, 'b) tlist \<Rightarrow> 'b"
   2.447 @@ -1731,14 +1731,14 @@
   2.448      | "termi\<^sub>0 (TCons x xs) = termi\<^sub>0 xs"
   2.449      end
   2.450  
   2.451 -text \<open> \blankline \<close>
   2.452 +text \<open>\blankline\<close>
   2.453  
   2.454      lemma termi_TCons[simp]: "termi (TCons x xs) = termi xs"
   2.455        by (cases xs) auto
   2.456  
   2.457  
   2.458 -subsection \<open> Compatibility Issues
   2.459 -  \label{ssec:primrec-compatibility-issues} \<close>
   2.460 +subsection \<open>Compatibility Issues
   2.461 +  \label{ssec:primrec-compatibility-issues}\<close>
   2.462  
   2.463  text \<open>
   2.464  The command @{command primrec}'s behavior on new-style datatypes has been
   2.465 @@ -1757,8 +1757,8 @@
   2.466  \<close>
   2.467  
   2.468  
   2.469 -section \<open> Defining Codatatypes
   2.470 -  \label{sec:defining-codatatypes} \<close>
   2.471 +section \<open>Defining Codatatypes
   2.472 +  \label{sec:defining-codatatypes}\<close>
   2.473  
   2.474  text \<open>
   2.475  Codatatypes can be specified using the @{command codatatype} command. The
   2.476 @@ -1770,11 +1770,11 @@
   2.477  \<close>
   2.478  
   2.479  
   2.480 -subsection \<open> Introductory Examples
   2.481 -  \label{ssec:codatatype-introductory-examples} \<close>
   2.482 -
   2.483 -subsubsection \<open> Simple Corecursion
   2.484 -  \label{sssec:codatatype-simple-corecursion} \<close>
   2.485 +subsection \<open>Introductory Examples
   2.486 +  \label{ssec:codatatype-introductory-examples}\<close>
   2.487 +
   2.488 +subsubsection \<open>Simple Corecursion
   2.489 +  \label{sssec:codatatype-simple-corecursion}\<close>
   2.490  
   2.491  text \<open>
   2.492  Non-corecursive codatatypes coincide with the corresponding datatypes, so they
   2.493 @@ -1836,8 +1836,8 @@
   2.494  \<close>
   2.495  
   2.496  
   2.497 -subsubsection \<open> Mutual Corecursion
   2.498 -  \label{sssec:codatatype-mutual-corecursion} \<close>
   2.499 +subsubsection \<open>Mutual Corecursion
   2.500 +  \label{sssec:codatatype-mutual-corecursion}\<close>
   2.501  
   2.502  text \<open>
   2.503  \noindent
   2.504 @@ -1848,8 +1848,8 @@
   2.505      and odd_enat = Odd_ESucc even_enat
   2.506  
   2.507  
   2.508 -subsubsection \<open> Nested Corecursion
   2.509 -  \label{sssec:codatatype-nested-corecursion} \<close>
   2.510 +subsubsection \<open>Nested Corecursion
   2.511 +  \label{sssec:codatatype-nested-corecursion}\<close>
   2.512  
   2.513  text \<open>
   2.514  \noindent
   2.515 @@ -1858,20 +1858,20 @@
   2.516  
   2.517      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")
   2.518  
   2.519 -text \<open> \blankline \<close>
   2.520 +text \<open>\blankline\<close>
   2.521  
   2.522      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")
   2.523  
   2.524 -text \<open> \blankline \<close>
   2.525 +text \<open>\blankline\<close>
   2.526  
   2.527      codatatype 'a sm = SM (accept: bool) (trans: "'a \<Rightarrow> 'a sm")
   2.528  
   2.529  
   2.530 -subsection \<open> Command Syntax
   2.531 -  \label{ssec:codatatype-command-syntax} \<close>
   2.532 -
   2.533 -subsubsection \<open> \keyw{codatatype}
   2.534 -  \label{sssec:codatatype} \<close>
   2.535 +subsection \<open>Command Syntax
   2.536 +  \label{ssec:codatatype-command-syntax}\<close>
   2.537 +
   2.538 +subsubsection \<open>\keyw{codatatype}
   2.539 +  \label{sssec:codatatype}\<close>
   2.540  
   2.541  text \<open>
   2.542  \begin{matharray}{rcl}
   2.543 @@ -1892,8 +1892,8 @@
   2.544  \<close>
   2.545  
   2.546  
   2.547 -subsection \<open> Generated Constants
   2.548 -  \label{ssec:codatatype-generated-constants} \<close>
   2.549 +subsection \<open>Generated Constants
   2.550 +  \label{ssec:codatatype-generated-constants}\<close>
   2.551  
   2.552  text \<open>
   2.553  Given a codatatype @{text "('a\<^sub>1, \<dots>, 'a\<^sub>m) t"}
   2.554 @@ -1911,8 +1911,8 @@
   2.555  \<close>
   2.556  
   2.557  
   2.558 -subsection \<open> Generated Theorems
   2.559 -  \label{ssec:codatatype-generated-theorems} \<close>
   2.560 +subsection \<open>Generated Theorems
   2.561 +  \label{ssec:codatatype-generated-theorems}\<close>
   2.562  
   2.563  text \<open>
   2.564  The characteristic theorems generated by @{command codatatype} are grouped in
   2.565 @@ -1938,8 +1938,8 @@
   2.566  \<close>
   2.567  
   2.568  
   2.569 -subsubsection \<open> Coinductive Theorems
   2.570 -  \label{sssec:coinductive-theorems} \<close>
   2.571 +subsubsection \<open>Coinductive Theorems
   2.572 +  \label{sssec:coinductive-theorems}\<close>
   2.573  
   2.574  text \<open>
   2.575  The coinductive theorems are listed below for @{typ "'a llist"}:
   2.576 @@ -2030,8 +2030,8 @@
   2.577  \<close>
   2.578  
   2.579  
   2.580 -section \<open> Defining Primitively Corecursive Functions
   2.581 -  \label{sec:defining-primitively-corecursive-functions} \<close>
   2.582 +section \<open>Defining Primitively Corecursive Functions
   2.583 +  \label{sec:defining-primitively-corecursive-functions}\<close>
   2.584  
   2.585  text \<open>
   2.586  Corecursive functions can be specified using the @{command primcorec} and
   2.587 @@ -2079,8 +2079,8 @@
   2.588  \<close>
   2.589  
   2.590  
   2.591 -subsection \<open> Introductory Examples
   2.592 -  \label{ssec:primcorec-introductory-examples} \<close>
   2.593 +subsection \<open>Introductory Examples
   2.594 +  \label{ssec:primcorec-introductory-examples}\<close>
   2.595  
   2.596  text \<open>
   2.597  Primitive corecursion is illustrated through concrete examples based on the
   2.598 @@ -2092,8 +2092,8 @@
   2.599  \<close>
   2.600  
   2.601  
   2.602 -subsubsection \<open> Simple Corecursion
   2.603 -  \label{sssec:primcorec-simple-corecursion} \<close>
   2.604 +subsubsection \<open>Simple Corecursion
   2.605 +  \label{sssec:primcorec-simple-corecursion}\<close>
   2.606  
   2.607  text \<open>
   2.608  Following the code view, corecursive calls are allowed on the right-hand side as
   2.609 @@ -2104,7 +2104,7 @@
   2.610      primcorec (*<*)(transfer) (*>*)literate :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a llist" where
   2.611        "literate g x = LCons x (literate g (g x))"
   2.612  
   2.613 -text \<open> \blankline \<close>
   2.614 +text \<open>\blankline\<close>
   2.615  
   2.616      primcorec siterate :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a stream" where
   2.617        "siterate g x = SCons x (siterate g (g x))"
   2.618 @@ -2201,8 +2201,8 @@
   2.619  \<close>
   2.620  
   2.621  
   2.622 -subsubsection \<open> Mutual Corecursion
   2.623 -  \label{sssec:primcorec-mutual-corecursion} \<close>
   2.624 +subsubsection \<open>Mutual Corecursion
   2.625 +  \label{sssec:primcorec-mutual-corecursion}\<close>
   2.626  
   2.627  text \<open>
   2.628  The syntax for mutually corecursive functions over mutually corecursive
   2.629 @@ -2217,8 +2217,8 @@
   2.630      | "odd_infty = Odd_ESucc even_infty"
   2.631  
   2.632  
   2.633 -subsubsection \<open> Nested Corecursion
   2.634 -  \label{sssec:primcorec-nested-corecursion} \<close>
   2.635 +subsubsection \<open>Nested Corecursion
   2.636 +  \label{sssec:primcorec-nested-corecursion}\<close>
   2.637  
   2.638  text \<open>
   2.639  The next pair of examples generalize the @{const literate} and @{const siterate}
   2.640 @@ -2231,7 +2231,7 @@
   2.641      primcorec iterate\<^sub>i\<^sub>i :: "('a \<Rightarrow> 'a llist) \<Rightarrow> 'a \<Rightarrow> 'a tree\<^sub>i\<^sub>i" where
   2.642        "iterate\<^sub>i\<^sub>i g x = Node\<^sub>i\<^sub>i x (lmap (iterate\<^sub>i\<^sub>i g) (g x))"
   2.643  
   2.644 -text \<open> \blankline \<close>
   2.645 +text \<open>\blankline\<close>
   2.646  
   2.647      primcorec iterate\<^sub>i\<^sub>s :: "('a \<Rightarrow> 'a fset) \<Rightarrow> 'a \<Rightarrow> 'a tree\<^sub>i\<^sub>s" where
   2.648        "iterate\<^sub>i\<^sub>s g x = Node\<^sub>i\<^sub>s x (fimage (iterate\<^sub>i\<^sub>s g) (g x))"
   2.649 @@ -2285,17 +2285,17 @@
   2.650      primcorec sm_of_dfa :: "('q \<Rightarrow> 'a \<Rightarrow> 'q) \<Rightarrow> 'q set \<Rightarrow> 'q \<Rightarrow> 'a sm" where
   2.651        "sm_of_dfa \<delta> F q = SM (q \<in> F) (\<lambda>a. sm_of_dfa \<delta> F (\<delta> q a))"
   2.652  
   2.653 -text \<open> \blankline \<close>
   2.654 +text \<open>\blankline\<close>
   2.655  
   2.656      primcorec empty_sm :: "'a sm" where
   2.657        "empty_sm = SM False (\<lambda>_. empty_sm)"
   2.658  
   2.659 -text \<open> \blankline \<close>
   2.660 +text \<open>\blankline\<close>
   2.661  
   2.662      primcorec not_sm :: "'a sm \<Rightarrow> 'a sm" where
   2.663        "not_sm M = SM (\<not> accept M) (\<lambda>a. not_sm (trans M a))"
   2.664  
   2.665 -text \<open> \blankline \<close>
   2.666 +text \<open>\blankline\<close>
   2.667  
   2.668      primcorec or_sm :: "'a sm \<Rightarrow> 'a sm \<Rightarrow> 'a sm" where
   2.669        "or_sm M N =
   2.670 @@ -2311,14 +2311,14 @@
   2.671      codatatype ('a, 'b) sm2 =
   2.672        SM2 (accept2: bool) (trans2: "'a \<Rightarrow> 'b \<Rightarrow> ('a, 'b) sm2")
   2.673  
   2.674 -text \<open> \blankline \<close>
   2.675 +text \<open>\blankline\<close>
   2.676  
   2.677      primcorec
   2.678        (*<*)(in early) (*>*)sm2_of_dfa :: "('q \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'q) \<Rightarrow> 'q set \<Rightarrow> 'q \<Rightarrow> ('a, 'b) sm2"
   2.679      where
   2.680        "sm2_of_dfa \<delta> F q = SM2 (q \<in> F) (op \<circ> (op \<circ> (sm2_of_dfa \<delta> F)) (\<delta> q))"
   2.681  
   2.682 -text \<open> \blankline \<close>
   2.683 +text \<open>\blankline\<close>
   2.684  
   2.685      primcorec
   2.686        sm2_of_dfa :: "('q \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'q) \<Rightarrow> 'q set \<Rightarrow> 'q \<Rightarrow> ('a, 'b) sm2"
   2.687 @@ -2326,8 +2326,8 @@
   2.688        "sm2_of_dfa \<delta> F q = SM2 (q \<in> F) (\<lambda>a b. sm2_of_dfa \<delta> F (\<delta> q a b))"
   2.689  
   2.690  
   2.691 -subsubsection \<open> Nested-as-Mutual Corecursion
   2.692 -  \label{sssec:primcorec-nested-as-mutual-corecursion} \<close>
   2.693 +subsubsection \<open>Nested-as-Mutual Corecursion
   2.694 +  \label{sssec:primcorec-nested-as-mutual-corecursion}\<close>
   2.695  
   2.696  text \<open>
   2.697  Just as it is possible to recurse over nested recursive datatypes as if they
   2.698 @@ -2366,8 +2366,8 @@
   2.699  (*>*)
   2.700  
   2.701  
   2.702 -subsubsection \<open> Constructor View
   2.703 -  \label{ssec:primrec-constructor-view} \<close>
   2.704 +subsubsection \<open>Constructor View
   2.705 +  \label{ssec:primrec-constructor-view}\<close>
   2.706  
   2.707  (*<*)
   2.708      locale ctr_view
   2.709 @@ -2437,8 +2437,8 @@
   2.710  \<close>
   2.711  
   2.712  
   2.713 -subsubsection \<open> Destructor View
   2.714 -  \label{ssec:primrec-destructor-view} \<close>
   2.715 +subsubsection \<open>Destructor View
   2.716 +  \label{ssec:primrec-destructor-view}\<close>
   2.717  
   2.718  (*<*)
   2.719      locale dtr_view
   2.720 @@ -2457,13 +2457,13 @@
   2.721      | "lhd (literate _ x) = x"
   2.722      | "ltl (literate g x) = literate g (g x)"
   2.723  
   2.724 -text \<open> \blankline \<close>
   2.725 +text \<open>\blankline\<close>
   2.726  
   2.727      primcorec siterate :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a stream" where
   2.728        "shd (siterate _ x) = x"
   2.729      | "stl (siterate g x) = siterate g (g x)"
   2.730  
   2.731 -text \<open> \blankline \<close>
   2.732 +text \<open>\blankline\<close>
   2.733  
   2.734      primcorec every_snd :: "'a stream \<Rightarrow> 'a stream" where
   2.735        "shd (every_snd s) = shd s"
   2.736 @@ -2544,7 +2544,7 @@
   2.737      | "un_Even_ESucc even_infty = odd_infty"
   2.738      | "un_Odd_ESucc odd_infty = even_infty"
   2.739  
   2.740 -text \<open> \blankline \<close>
   2.741 +text \<open>\blankline\<close>
   2.742  
   2.743      primcorec iterate\<^sub>i\<^sub>i :: "('a \<Rightarrow> 'a llist) \<Rightarrow> 'a \<Rightarrow> 'a tree\<^sub>i\<^sub>i" where
   2.744        "lbl\<^sub>i\<^sub>i (iterate\<^sub>i\<^sub>i g x) = x"
   2.745 @@ -2554,11 +2554,11 @@
   2.746  (*>*)
   2.747  
   2.748  
   2.749 -subsection \<open> Command Syntax
   2.750 -  \label{ssec:primcorec-command-syntax} \<close>
   2.751 -
   2.752 -subsubsection \<open> \keyw{primcorec} and \keyw{primcorecursive}
   2.753 -  \label{sssec:primcorecursive-and-primcorec} \<close>
   2.754 +subsection \<open>Command Syntax
   2.755 +  \label{ssec:primcorec-command-syntax}\<close>
   2.756 +
   2.757 +subsubsection \<open>\keyw{primcorec} and \keyw{primcorecursive}
   2.758 +  \label{sssec:primcorecursive-and-primcorec}\<close>
   2.759  
   2.760  text \<open>
   2.761  \begin{matharray}{rcl}
   2.762 @@ -2621,8 +2621,8 @@
   2.763  \<close>
   2.764  
   2.765  
   2.766 -subsection \<open> Generated Theorems
   2.767 -  \label{ssec:primcorec-generated-theorems} \<close>
   2.768 +subsection \<open>Generated Theorems
   2.769 +  \label{ssec:primcorec-generated-theorems}\<close>
   2.770  
   2.771  text \<open>
   2.772  The @{command primcorec} and @{command primcorecursive} commands generate the
   2.773 @@ -2719,8 +2719,8 @@
   2.774  
   2.775  
   2.776  (*
   2.777 -subsection \<open> Recursive Default Values for Selectors
   2.778 -  \label{ssec:primcorec-recursive-default-values-for-selectors} \<close>
   2.779 +subsection \<open>Recursive Default Values for Selectors
   2.780 +  \label{ssec:primcorec-recursive-default-values-for-selectors}\<close>
   2.781  
   2.782  text \<open>
   2.783  partial_function to the rescue
   2.784 @@ -2728,8 +2728,8 @@
   2.785  *)
   2.786  
   2.787  
   2.788 -section \<open> Registering Bounded Natural Functors
   2.789 -  \label{sec:registering-bounded-natural-functors} \<close>
   2.790 +section \<open>Registering Bounded Natural Functors
   2.791 +  \label{sec:registering-bounded-natural-functors}\<close>
   2.792  
   2.793  text \<open>
   2.794  The (co)datatype package can be set up to allow nested recursion through
   2.795 @@ -2739,8 +2739,8 @@
   2.796  \<close>
   2.797  
   2.798  
   2.799 -subsection \<open> Bounded Natural Functors
   2.800 -  \label{ssec:bounded-natural-functors} \<close>
   2.801 +subsection \<open>Bounded Natural Functors
   2.802 +  \label{ssec:bounded-natural-functors}\<close>
   2.803  
   2.804  text \<open>
   2.805  Bounded natural functors (BNFs) are a semantic criterion for where
   2.806 @@ -2773,8 +2773,8 @@
   2.807  \<close>
   2.808  
   2.809  
   2.810 -subsection \<open> Introductory Examples
   2.811 -  \label{ssec:bnf-introductory-examples} \<close>
   2.812 +subsection \<open>Introductory Examples
   2.813 +  \label{ssec:bnf-introductory-examples}\<close>
   2.814  
   2.815  text \<open>
   2.816  The example below shows how to register a type as a BNF using the @{command bnf}
   2.817 @@ -2789,16 +2789,16 @@
   2.818      typedef ('d, 'a) fn = "UNIV :: ('d \<Rightarrow> 'a) set"
   2.819        by simp
   2.820  
   2.821 -text \<open> \blankline \<close>
   2.822 +text \<open>\blankline\<close>
   2.823  
   2.824      setup_lifting type_definition_fn
   2.825  
   2.826 -text \<open> \blankline \<close>
   2.827 +text \<open>\blankline\<close>
   2.828  
   2.829      lift_definition map_fn :: "('a \<Rightarrow> 'b) \<Rightarrow> ('d, 'a) fn \<Rightarrow> ('d, 'b) fn" is "op \<circ>" .
   2.830      lift_definition set_fn :: "('d, 'a) fn \<Rightarrow> 'a set" is range .
   2.831  
   2.832 -text \<open> \blankline \<close>
   2.833 +text \<open>\blankline\<close>
   2.834  
   2.835      lift_definition
   2.836        pred_fn :: "('a \<Rightarrow> bool) \<Rightarrow> ('d, 'a) fn \<Rightarrow> bool"
   2.837 @@ -2810,7 +2810,7 @@
   2.838      is
   2.839        "rel_fun (op =)" .
   2.840  
   2.841 -text \<open> \blankline \<close>
   2.842 +text \<open>\blankline\<close>
   2.843  
   2.844      bnf "('d, 'a) fn"
   2.845        map: map_fn
   2.846 @@ -2866,7 +2866,7 @@
   2.847          unfolding fun_eq_iff by transfer simp
   2.848      qed
   2.849  
   2.850 -text \<open> \blankline \<close>
   2.851 +text \<open>\blankline\<close>
   2.852  
   2.853      print_theorems
   2.854      print_bnfs
   2.855 @@ -2925,7 +2925,7 @@
   2.856        xval :: 'a
   2.857        yval :: 'a
   2.858  
   2.859 -text \<open> \blankline \<close>
   2.860 +text \<open>\blankline\<close>
   2.861  
   2.862      copy_bnf ('a, 'z) point_ext
   2.863  
   2.864 @@ -2970,17 +2970,17 @@
   2.865      bnf_axiomatization (setA: 'a, setB: 'b, setC: 'c) F
   2.866        [wits: "'a \<Rightarrow> ('a, 'b, 'c) F"]
   2.867  
   2.868 -text \<open> \blankline \<close>
   2.869 +text \<open>\blankline\<close>
   2.870  
   2.871      print_theorems
   2.872      print_bnfs
   2.873  
   2.874  
   2.875 -subsection \<open> Command Syntax
   2.876 -  \label{ssec:bnf-command-syntax} \<close>
   2.877 -
   2.878 -subsubsection \<open> \keyw{bnf}
   2.879 -  \label{sssec:bnf} \<close>
   2.880 +subsection \<open>Command Syntax
   2.881 +  \label{ssec:bnf-command-syntax}\<close>
   2.882 +
   2.883 +subsubsection \<open>\keyw{bnf}
   2.884 +  \label{sssec:bnf}\<close>
   2.885  
   2.886  text \<open>
   2.887  \begin{matharray}{rcl}
   2.888 @@ -3012,8 +3012,8 @@
   2.889  %%% TODO: elaborate on proof obligations
   2.890  \<close>
   2.891  
   2.892 -subsubsection \<open> \keyw{lift_bnf}
   2.893 -  \label{sssec:lift-bnf} \<close>
   2.894 +subsubsection \<open>\keyw{lift_bnf}
   2.895 +  \label{sssec:lift-bnf}\<close>
   2.896  
   2.897  text \<open>
   2.898  \begin{matharray}{rcl}
   2.899 @@ -3048,8 +3048,8 @@
   2.900  specifying the @{text no_warn_wits} option.
   2.901  \<close>
   2.902  
   2.903 -subsubsection \<open> \keyw{copy_bnf}
   2.904 -  \label{sssec:copy-bnf} \<close>
   2.905 +subsubsection \<open>\keyw{copy_bnf}
   2.906 +  \label{sssec:copy-bnf}\<close>
   2.907  
   2.908  text \<open>
   2.909  \begin{matharray}{rcl}
   2.910 @@ -3069,8 +3069,8 @@
   2.911  nonemptiness witnesses.
   2.912  \<close>
   2.913  
   2.914 -subsubsection \<open> \keyw{bnf_axiomatization}
   2.915 -  \label{sssec:bnf-axiomatization} \<close>
   2.916 +subsubsection \<open>\keyw{bnf_axiomatization}
   2.917 +  \label{sssec:bnf-axiomatization}\<close>
   2.918  
   2.919  text \<open>
   2.920  \begin{matharray}{rcl}
   2.921 @@ -3114,8 +3114,8 @@
   2.922  \<close>
   2.923  
   2.924  
   2.925 -subsubsection \<open> \keyw{print_bnfs}
   2.926 -  \label{sssec:print-bnfs} \<close>
   2.927 +subsubsection \<open>\keyw{print_bnfs}
   2.928 +  \label{sssec:print-bnfs}\<close>
   2.929  
   2.930  text \<open>
   2.931  \begin{matharray}{rcl}
   2.932 @@ -3128,8 +3128,8 @@
   2.933  \<close>
   2.934  
   2.935  
   2.936 -section \<open> Deriving Destructors and Theorems for Free Constructors
   2.937 -  \label{sec:deriving-destructors-and-theorems-for-free-constructors} \<close>
   2.938 +section \<open>Deriving Destructors and Theorems for Free Constructors
   2.939 +  \label{sec:deriving-destructors-and-theorems-for-free-constructors}\<close>
   2.940  
   2.941  text \<open>
   2.942  The derivation of convenience theorems for types equipped with free constructors,
   2.943 @@ -3146,16 +3146,16 @@
   2.944  
   2.945  
   2.946  (*
   2.947 -subsection \<open> Introductory Example
   2.948 -  \label{ssec:ctors-introductory-example} \<close>
   2.949 +subsection \<open>Introductory Example
   2.950 +  \label{ssec:ctors-introductory-example}\<close>
   2.951  *)
   2.952  
   2.953  
   2.954 -subsection \<open> Command Syntax
   2.955 -  \label{ssec:ctors-command-syntax} \<close>
   2.956 -
   2.957 -subsubsection \<open> \keyw{free_constructors}
   2.958 -  \label{sssec:free-constructors} \<close>
   2.959 +subsection \<open>Command Syntax
   2.960 +  \label{ssec:ctors-command-syntax}\<close>
   2.961 +
   2.962 +subsubsection \<open>\keyw{free_constructors}
   2.963 +  \label{sssec:free-constructors}\<close>
   2.964  
   2.965  text \<open>
   2.966  \begin{matharray}{rcl}
   2.967 @@ -3195,8 +3195,8 @@
   2.968  \<close>
   2.969  
   2.970  
   2.971 -subsubsection \<open> \keyw{simps_of_case}
   2.972 -  \label{sssec:simps-of-case} \<close>
   2.973 +subsubsection \<open>\keyw{simps_of_case}
   2.974 +  \label{sssec:simps-of-case}\<close>
   2.975  
   2.976  text \<open>
   2.977  \begin{matharray}{rcl}
   2.978 @@ -3234,8 +3234,8 @@
   2.979  \<close>
   2.980  
   2.981  
   2.982 -subsubsection \<open> \keyw{case_of_simps}
   2.983 -  \label{sssec:case-of-simps} \<close>
   2.984 +subsubsection \<open>\keyw{case_of_simps}
   2.985 +  \label{sssec:case-of-simps}\<close>
   2.986  
   2.987  text \<open>
   2.988  \begin{matharray}{rcl}
   2.989 @@ -3275,8 +3275,8 @@
   2.990  
   2.991  
   2.992  (*
   2.993 -section \<open> Using the Standard ML Interface
   2.994 -  \label{sec:using-the-standard-ml-interface} \<close>
   2.995 +section \<open>Using the Standard ML Interface
   2.996 +  \label{sec:using-the-standard-ml-interface}\<close>
   2.997  
   2.998  text \<open>
   2.999  The package's programmatic interface.
  2.1000 @@ -3284,8 +3284,8 @@
  2.1001  *)
  2.1002  
  2.1003  
  2.1004 -section \<open> Selecting Plugins
  2.1005 -  \label{sec:selecting-plugins} \<close>
  2.1006 +section \<open>Selecting Plugins
  2.1007 +  \label{sec:selecting-plugins}\<close>
  2.1008  
  2.1009  text \<open>
  2.1010  Plugins extend the (co)datatype package to interoperate with other Isabelle
  2.1011 @@ -3305,8 +3305,8 @@
  2.1012  @{cite "sternagel-thiemann-2015"}.
  2.1013  \<close>
  2.1014  
  2.1015 -subsection \<open> Code Generator
  2.1016 -  \label{ssec:code-generator} \<close>
  2.1017 +subsection \<open>Code Generator
  2.1018 +  \label{ssec:code-generator}\<close>
  2.1019  
  2.1020  text \<open>
  2.1021  The \hthm{code} plugin registers freely generated types, including
  2.1022 @@ -3342,8 +3342,8 @@
  2.1023  \<close>
  2.1024  
  2.1025  
  2.1026 -subsection \<open> Size
  2.1027 -  \label{ssec:size} \<close>
  2.1028 +subsection \<open>Size
  2.1029 +  \label{ssec:size}\<close>
  2.1030  
  2.1031  text \<open>
  2.1032  For each datatype @{text t}, the \hthm{size} plugin generates a generic size
  2.1033 @@ -3392,8 +3392,8 @@
  2.1034  \<close>
  2.1035  
  2.1036  
  2.1037 -subsection \<open> Transfer
  2.1038 -  \label{ssec:transfer} \<close>
  2.1039 +subsection \<open>Transfer
  2.1040 +  \label{ssec:transfer}\<close>
  2.1041  
  2.1042  text \<open>
  2.1043  For each (co)datatype with live type arguments and each manually registered BNF,
  2.1044 @@ -3451,8 +3451,8 @@
  2.1045  \<close>
  2.1046  
  2.1047  
  2.1048 -subsection \<open> Lifting
  2.1049 -  \label{ssec:lifting} \<close>
  2.1050 +subsection \<open>Lifting
  2.1051 +  \label{ssec:lifting}\<close>
  2.1052  
  2.1053  text \<open>
  2.1054  For each (co)datatype and each manually registered BNF with at least one live
  2.1055 @@ -3477,8 +3477,8 @@
  2.1056  \<close>
  2.1057  
  2.1058  
  2.1059 -subsection \<open> Quickcheck
  2.1060 -  \label{ssec:quickcheck} \<close>
  2.1061 +subsection \<open>Quickcheck
  2.1062 +  \label{ssec:quickcheck}\<close>
  2.1063  
  2.1064  text \<open>
  2.1065  The integration of datatypes with Quickcheck is accomplished by the
  2.1066 @@ -3496,8 +3496,8 @@
  2.1067  \<close>
  2.1068  
  2.1069  
  2.1070 -subsection \<open> Program Extraction
  2.1071 -  \label{ssec:program-extraction} \<close>
  2.1072 +subsection \<open>Program Extraction
  2.1073 +  \label{ssec:program-extraction}\<close>
  2.1074  
  2.1075  text \<open>
  2.1076  The \hthm{extraction} plugin provides realizers for induction and case analysis,
  2.1077 @@ -3507,13 +3507,12 @@
  2.1078  \<close>
  2.1079  
  2.1080  
  2.1081 -section \<open> Known Bugs and Limitations
  2.1082 -  \label{sec:known-bugs-and-limitations} \<close>
  2.1083 +section \<open>Known Bugs and Limitations
  2.1084 +  \label{sec:known-bugs-and-limitations}\<close>
  2.1085  
  2.1086  text \<open>
  2.1087 -This section lists the known bugs and limitations in the (co)datatype package at
  2.1088 -the time of this writing. Many of them are expected to be addressed in future
  2.1089 -releases.
  2.1090 +This section lists the known bugs and limitations of the (co)datatype package at
  2.1091 +the time of this writing.
  2.1092  
  2.1093  \begin{enumerate}
  2.1094  \setlength{\itemsep}{0pt}