| changeset 58889 | 5b7a9633cfa8 |
| parent 58396 | 7b60e4e74430 |
| child 61260 | e6f03fae14d5 |
--- a/src/HOL/Datatype_Examples/Misc_N2M.thy Sun Nov 02 18:21:14 2014 +0100 +++ b/src/HOL/Datatype_Examples/Misc_N2M.thy Sun Nov 02 18:21:45 2014 +0100 @@ -5,7 +5,7 @@ Miscellaneous tests for the nested-to-mutual reduction. *) -header \<open>Miscellaneous Tests for the Nested-to-Mutual Reduction\<close> +section \<open>Miscellaneous Tests for the Nested-to-Mutual Reduction\<close> theory Misc_N2M imports "~~/src/HOL/Library/BNF_Axiomatization"