src/HOL/Smallcheck.thy
changeset 40620 7a9278de19ad
parent 40420 552563ea3304
child 40639 f1f0e6adca0a
     1.1 --- a/src/HOL/Smallcheck.thy	Wed Nov 17 11:07:02 2010 -0800
     1.2 +++ b/src/HOL/Smallcheck.thy	Wed Nov 17 11:39:44 2010 -0800
     1.3 @@ -8,7 +8,7 @@
     1.4  begin
     1.5  
     1.6  
     1.7 -section {* small value generator type classes *}
     1.8 +subsection {* small value generator type classes *}
     1.9  
    1.10  class small = term_of +
    1.11  fixes small :: "('a \<Rightarrow> term list option) \<Rightarrow> code_numeral \<Rightarrow> term list option"
    1.12 @@ -48,7 +48,7 @@
    1.13  
    1.14  end
    1.15  
    1.16 -section {* Defining combinators for any first-order data type *}
    1.17 +subsection {* Defining combinators for any first-order data type *}
    1.18  
    1.19  definition catch_match :: "term list option => term list option => term list option"
    1.20  where