tuned document;

--- a/src/HOL/UNITY/Comp/Alloc.thy	Tue Jan 16 09:58:06 2018 +0100
+++ b/src/HOL/UNITY/Comp/Alloc.thy	Tue Jan 16 09:58:17 2018 +0100
@@ -47,7 +47,7 @@
   dummy  :: 'a                    \<comment> \<open>dummy field for new variables\<close>
 
 
-\<comment> \<open>* Resource allocation system specification *\<close>
+subsubsection \<open>Resource allocation system specification\<close>
 
 definition
   \<comment> \<open>spec (1)\<close>
@@ -68,7 +68,8 @@
   system_spec :: "'a systemState program set"
   where "system_spec = system_safety Int system_progress"
 
-\<comment> \<open>* Client specification (required) **\<close>
+
+subsubsection \<open>Client specification (required)\<close>
 
 definition
   \<comment> \<open>spec (3)\<close>
@@ -105,7 +106,8 @@
   where "client_spec = client_increasing Int client_bounded Int client_progress
                     Int client_allowed_acts Int client_preserves"
 
-\<comment> \<open>* Allocator specification (required) *\<close>
+
+subsubsection \<open>Allocator specification (required)\<close>
 
 definition
   \<comment> \<open>spec (6)\<close>
@@ -168,7 +170,8 @@
   where "alloc_spec = alloc_increasing Int alloc_safety Int alloc_progress Int
                    alloc_allowed_acts Int alloc_preserves"
 
-\<comment> \<open>* Network specification *\<close>
+
+subsubsection \<open>Network specification\<close>
 
 definition
   \<comment> \<open>spec (9.1)\<close>
@@ -218,7 +221,8 @@
                      network_preserves"
 
 
-\<comment> \<open>* State mappings *\<close>
+subsubsection \<open>State mappings\<close>
+
 definition
   sysOfAlloc :: "((nat => clientState) * 'a) allocState_d => 'a systemState"
   where "sysOfAlloc = (%s. let (cl,xtr) = allocState_d.dummy s

--- a/src/ZF/UNITY/Mutex.thy	Tue Jan 16 09:58:06 2018 +0100
+++ b/src/ZF/UNITY/Mutex.thy	Tue Jan 16 09:58:17 2018 +0100
@@ -27,7 +27,7 @@
 abbreviation "u == Var([0,1])"
 abbreviation "v == Var([1,0])"
 
-axiomatization where \<comment> \<open>* Type declarations  *\<close>
+axiomatization where \<comment> \<open>Type declarations\<close>
   p_type:  "type_of(p)=bool & default_val(p)=0" and
   m_type:  "type_of(m)=int  & default_val(m)=#0" and
   n_type:  "type_of(n)=int  & default_val(n)=#0" and