--- a/src/HOL/Library/Cancellation.thy Mon Apr 10 23:21:47 2023 +0200
+++ b/src/HOL/Library/Cancellation.thy Tue Apr 11 11:59:02 2023 +0000
@@ -74,7 +74,7 @@
by (auto dest!: le_Suc_ex add_right_imp_eq simp: ab_semigroup_add_class.add_ac(1))
-subsection \<open>Simproc Set-Up\<close>
+text \<open>Simproc Set-Up\<close>
ML_file \<open>Cancellation/cancel.ML\<close>
ML_file \<open>Cancellation/cancel_data.ML\<close>
--- a/src/HOL/Library/Case_Converter.thy Mon Apr 10 23:21:47 2023 +0200
+++ b/src/HOL/Library/Case_Converter.thy Tue Apr 11 11:59:02 2023 +0000
@@ -1,12 +1,12 @@
(* Author: Pascal Stoop, ETH Zurich
Author: Andreas Lochbihler, Digital Asset *)
+section \<open>Eliminating pattern matches\<close>
+
theory Case_Converter
imports Main
begin
-subsection \<open>Eliminating pattern matches\<close>
-
definition missing_pattern_match :: "String.literal \<Rightarrow> (unit \<Rightarrow> 'a) \<Rightarrow> 'a" where
[code del]: "missing_pattern_match m f = f ()"
--- a/src/HOL/Library/Code_Cardinality.thy Mon Apr 10 23:21:47 2023 +0200
+++ b/src/HOL/Library/Code_Cardinality.thy Tue Apr 11 11:59:02 2023 +0000
@@ -1,4 +1,4 @@
-subsection \<open>Code setup for sets with cardinality type information\<close>
+section \<open>Code setup for sets with cardinality type information\<close>
theory Code_Cardinality imports Cardinality begin
--- a/src/HOL/Library/Code_Test.thy Mon Apr 10 23:21:47 2023 +0200
+++ b/src/HOL/Library/Code_Test.thy Tue Apr 11 11:59:02 2023 +0000
@@ -4,6 +4,8 @@
Test infrastructure for the code generator.
*)
+section \<open>Test infrastructure for the code generator\<close>
+
theory Code_Test
imports Main
keywords "test_code" :: diag
--- a/src/HOL/Library/Extended_Nonnegative_Real.thy Mon Apr 10 23:21:47 2023 +0200
+++ b/src/HOL/Library/Extended_Nonnegative_Real.thy Tue Apr 11 11:59:02 2023 +0000
@@ -2,7 +2,7 @@
Author: Johannes Hölzl
*)
-subsection \<open>The type of non-negative extended real numbers\<close>
+section \<open>The type of non-negative extended real numbers\<close>
theory Extended_Nonnegative_Real
imports Extended_Real Indicator_Function
--- a/src/HOL/Library/Finite_Lattice.thy Mon Apr 10 23:21:47 2023 +0200
+++ b/src/HOL/Library/Finite_Lattice.thy Tue Apr 11 11:59:02 2023 +0000
@@ -2,10 +2,14 @@
Author: Alessandro Coglio
*)
+section \<open>Finite Lattices\<close>
+
theory Finite_Lattice
imports Product_Order
begin
+subsection \<open>Finite Complete Lattices\<close>
+
text \<open>A non-empty finite lattice is a complete lattice.
Since types are never empty in Isabelle/HOL,
a type of classes \<^class>\<open>finite\<close> and \<^class>\<open>lattice\<close>
--- a/src/HOL/Library/Lattice_Constructions.thy Mon Apr 10 23:21:47 2023 +0200
+++ b/src/HOL/Library/Lattice_Constructions.thy Tue Apr 11 11:59:02 2023 +0000
@@ -3,12 +3,12 @@
Copyright 2010 TU Muenchen
*)
+section \<open>Values extended by a bottom element\<close>
+
theory Lattice_Constructions
imports Main
begin
-subsection \<open>Values extended by a bottom element\<close>
-
datatype 'a bot = Value 'a | Bot
instantiation bot :: (preorder) preorder
--- a/src/HOL/Library/Rounded_Division.thy Mon Apr 10 23:21:47 2023 +0200
+++ b/src/HOL/Library/Rounded_Division.thy Tue Apr 11 11:59:02 2023 +0000
@@ -1,7 +1,7 @@
(* Author: Florian Haftmann, TU Muenchen
*)
-subsection \<open>Rounded division: modulus centered towards zero.\<close>
+section \<open>Rounded division: modulus centered towards zero.\<close>
theory Rounded_Division
imports Main
--- a/src/HOL/Library/Signed_Division.thy Mon Apr 10 23:21:47 2023 +0200
+++ b/src/HOL/Library/Signed_Division.thy Tue Apr 11 11:59:02 2023 +0000
@@ -1,7 +1,7 @@
(* Author: Stefan Berghofer et al.
*)
-subsection \<open>Signed division: negative results rounded towards zero rather than minus infinity.\<close>
+section \<open>Signed division: negative results rounded towards zero rather than minus infinity.\<close>
theory Signed_Division
imports Main