src/HOL/Smallcheck.thy
changeset 40620 7a9278de19ad
parent 40420 552563ea3304
child 40639 f1f0e6adca0a
--- a/src/HOL/Smallcheck.thy	Wed Nov 17 11:07:02 2010 -0800
+++ b/src/HOL/Smallcheck.thy	Wed Nov 17 11:39:44 2010 -0800
@@ -8,7 +8,7 @@
 begin
 
 
-section {* small value generator type classes *}
+subsection {* small value generator type classes *}
 
 class small = term_of +
 fixes small :: "('a \<Rightarrow> term list option) \<Rightarrow> code_numeral \<Rightarrow> term list option"
@@ -48,7 +48,7 @@
 
 end
 
-section {* Defining combinators for any first-order data type *}
+subsection {* Defining combinators for any first-order data type *}
 
 definition catch_match :: "term list option => term list option => term list option"
 where