src/HOL/Quickcheck_Exhaustive.thy
changeset 60758 d8d85a8172b5
parent 59484 a130ae7a9398
child 61121 efe8b18306b7
     1.1 --- a/src/HOL/Quickcheck_Exhaustive.thy	Sat Jul 18 21:44:18 2015 +0200
     1.2 +++ b/src/HOL/Quickcheck_Exhaustive.thy	Sat Jul 18 22:58:50 2015 +0200
     1.3 @@ -1,19 +1,19 @@
     1.4  (* Author: Lukas Bulwahn, TU Muenchen *)
     1.5  
     1.6 -section {* A simple counterexample generator performing exhaustive testing *}
     1.7 +section \<open>A simple counterexample generator performing exhaustive testing\<close>
     1.8  
     1.9  theory Quickcheck_Exhaustive
    1.10  imports Quickcheck_Random
    1.11  keywords "quickcheck_generator" :: thy_decl
    1.12  begin
    1.13  
    1.14 -subsection {* basic operations for exhaustive generators *}
    1.15 +subsection \<open>basic operations for exhaustive generators\<close>
    1.16  
    1.17  definition orelse :: "'a option => 'a option => 'a option" (infixr "orelse" 55)
    1.18  where
    1.19    [code_unfold]: "x orelse y = (case x of Some x' => Some x' | None => y)"
    1.20  
    1.21 -subsection {* exhaustive generator type classes *}
    1.22 +subsection \<open>exhaustive generator type classes\<close>
    1.23  
    1.24  class exhaustive = term_of +
    1.25    fixes exhaustive :: "('a \<Rightarrow> (bool * term list) option) \<Rightarrow> natural \<Rightarrow> (bool * term list) option"
    1.26 @@ -229,7 +229,7 @@
    1.27  
    1.28  end
    1.29  
    1.30 -subsubsection {* A smarter enumeration scheme for functions over finite datatypes *}
    1.31 +subsubsection \<open>A smarter enumeration scheme for functions over finite datatypes\<close>
    1.32  
    1.33  class check_all = enum + term_of +
    1.34    fixes check_all :: "('a * (unit \<Rightarrow> term) \<Rightarrow> (bool * term list) option) \<Rightarrow> (bool * term list) option"
    1.35 @@ -505,12 +505,12 @@
    1.36  
    1.37  end
    1.38  
    1.39 -subsection {* Bounded universal quantifiers *}
    1.40 +subsection \<open>Bounded universal quantifiers\<close>
    1.41  
    1.42  class bounded_forall =
    1.43    fixes bounded_forall :: "('a \<Rightarrow> bool) \<Rightarrow> natural \<Rightarrow> bool"
    1.44  
    1.45 -subsection {* Fast exhaustive combinators *}
    1.46 +subsection \<open>Fast exhaustive combinators\<close>
    1.47  
    1.48  class fast_exhaustive = term_of +
    1.49    fixes fast_exhaustive :: "('a \<Rightarrow> unit) \<Rightarrow> natural \<Rightarrow> unit"
    1.50 @@ -524,7 +524,7 @@
    1.51  | constant catch_Counterexample \<rightharpoonup>
    1.52      (Quickcheck) "(((_); NONE) handle Exhaustive'_Generators.Counterexample ts => SOME ts)"
    1.53  
    1.54 -subsection {* Continuation passing style functions as plus monad *}
    1.55 +subsection \<open>Continuation passing style functions as plus monad\<close>
    1.56    
    1.57  type_synonym 'a cps = "('a => term list option) => term list option"
    1.58  
    1.59 @@ -610,7 +610,7 @@
    1.60  where
    1.61    "pos_bound_cps_not n = (%c i. case n (%u. Value []) i of No_value => c () | Value _ => None | Unknown_value => None)"
    1.62  
    1.63 -subsection {* Defining generators for any first-order data type *}
    1.64 +subsection \<open>Defining generators for any first-order data type\<close>
    1.65  
    1.66  axiomatization unknown :: 'a
    1.67  
    1.68 @@ -620,7 +620,7 @@
    1.69  
    1.70  declare [[quickcheck_batch_tester = exhaustive]]
    1.71  
    1.72 -subsection {* Defining generators for abstract types *}
    1.73 +subsection \<open>Defining generators for abstract types\<close>
    1.74  
    1.75  ML_file "Tools/Quickcheck/abstract_generators.ML"
    1.76