# HG changeset patch
# User blanchet
# Date 1411129443 -7200
# Node ID 7b60e4e74430f2b82a9d847f24a194343aa024c8
# Parent  7179d4da97fc173d68cd1bcd8436ba9b8ddf5e75
tuning

diff -r 7179d4da97fc -r 7b60e4e74430 src/HOL/Datatype_Examples/Misc_N2M.thy
--- a/src/HOL/Datatype_Examples/Misc_N2M.thy	Fri Sep 19 14:08:21 2014 +0200
+++ b/src/HOL/Datatype_Examples/Misc_N2M.thy	Fri Sep 19 14:24:03 2014 +0200
@@ -2,7 +2,7 @@
     Author:     Dmitriy Traytel, TU Muenchen
     Copyright   2014
 
-Miscellaneous datatype definitions.
+Miscellaneous tests for the nested-to-mutual reduction.
 *)
 
 header \<open>Miscellaneous Tests for the Nested-to-Mutual Reduction\<close>
@@ -126,8 +126,7 @@
 datatype_compat ll1 ll2
 
 
-
-section \<open>Deep Nesting\<close>
+subsection \<open>Deep Nesting\<close>
 
 datatype 'a tree = Empty | Node 'a "'a tree list"
 datatype_compat tree
@@ -156,7 +155,8 @@
 datatype_compat G
 datatype_compat H
 
-section \<open>Primrec cache\<close>
+
+subsection \<open>Primrec cache\<close>
 
 datatype 'a l = N | C 'a "'a l"
 datatype ('a, 'b) t = T 'a 'b "('a, 'b) t l"
@@ -331,8 +331,7 @@
   "l1_t4 (T4 n _ ts us) = n + l1_tl5 ts + l1_tl6 us"
 
 
-
-section \<open>Primcorec Cache\<close>
+subsection \<open>Primcorec Cache\<close>
 
 codatatype 'a col = N | C 'a "'a col"
 codatatype ('a, 'b) cot = T 'a 'b "('a, 'b) cot col"