
diff -r 26c3a9c92e11 -r a97ec0954c50 src/Pure/ex/Alternative_Headings_Examples.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/ex/Alternative_Headings_Examples.thy	Tue Nov 23 21:02:13 2021 +0100
@@ -0,0 +1,23 @@
+(*  Title:      Pure/ex/Alternative_Headings_Examples.thy
+    Author:     Makarius
+*)
+
+chapter \<open>Some examples of alternative document headings\<close>
+
+theory Alternative_Headings_Examples
+  imports Alternative_Headings
+begin
+
+section \<open>Regular section\<close>
+
+subsection \<open>Regular subsection\<close>
+
+subsubsection \<open>Regular subsubsection\<close>
+
+subsubsection* \<open>Alternative subsubsection\<close>
+
+subsection* \<open>Alternative subsection\<close>
+
+section* \<open>Alternative section\<close>
+
+end




