# HG changeset patch
# User haftmann
# Date 1681214342 0
# Node ID ae9e6218443dda4b7da49e5c842d9fd8254f803d
# Parent  1a9decb8bfbcf4151e86a53c96a2f97827d642a4
proper section headings

diff -r 1a9decb8bfbc -r ae9e6218443d src/HOL/Library/Cancellation.thy
--- 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>
diff -r 1a9decb8bfbc -r ae9e6218443d src/HOL/Library/Case_Converter.thy
--- 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 ()"
 
diff -r 1a9decb8bfbc -r ae9e6218443d src/HOL/Library/Code_Cardinality.thy
--- 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
 
diff -r 1a9decb8bfbc -r ae9e6218443d src/HOL/Library/Code_Test.thy
--- 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
diff -r 1a9decb8bfbc -r ae9e6218443d src/HOL/Library/Extended_Nonnegative_Real.thy
--- 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
diff -r 1a9decb8bfbc -r ae9e6218443d src/HOL/Library/Finite_Lattice.thy
--- 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>
diff -r 1a9decb8bfbc -r ae9e6218443d src/HOL/Library/Lattice_Constructions.thy
--- 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
diff -r 1a9decb8bfbc -r ae9e6218443d src/HOL/Library/Rounded_Division.thy
--- 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
diff -r 1a9decb8bfbc -r ae9e6218443d src/HOL/Library/Signed_Division.thy
--- 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