src/HOL/Quickcheck_Examples/Quickcheck_Interfaces.thy

 theory Quickcheck_Interfaces
 imports Main
 begin
 
-subsection {* Checking a single proposition (TODO) *}
+subsection \<open>Checking a single proposition (TODO)\<close>
 
-subsection {* Checking multiple propositions in one batch *}
+subsection \<open>Checking multiple propositions in one batch\<close>
 
-text {*
+text \<open>
 
 First, this requires to setup special generators for all datatypes via the following command.
-*}
+\<close>
 
 setup Exhaustive_Generators.setup_bounded_forall_datatype_interpretation
 
-text {*
+text \<open>
 Now, the function Quickcheck.mk_batch_validator : Proof.context -> term list -> (int -> bool) list option
 takes formulas of type bool with free variables, and returns a list of testing functions.
-*}
+\<close>
 
-ML {*
+ML \<open>
 val SOME testers = Quickcheck.mk_batch_validator @{context}
   [@{term "x = (1 :: nat)"}, @{term "x = (0 :: nat)"}, @{term "x <= (5 :: nat)"}, @{term "0 \<le> (x :: nat)"}]
-*}
+\<close>
 
-text {*
+text \<open>
 It is up to the user with which strategy the conjectures should be tested.
 For example, one could check all conjectures up to a given size, and check the different conjectures in sequence.
 This is implemented by:
-*}
+\<close>
 
-ML {*
+ML \<open>
 fun check_upto f i j = if i > j then true else f i andalso check_upto f (i + 1) j
-*}
+\<close>
 
-ML_val {* 
+ML_val \<open>
   map (fn test => check_upto test 0 1) testers
-*}
-ML_val {* 
+\<close>
+ML_val \<open>
   map (fn test => check_upto test 0 2) testers
-*}
-ML_val {* 
+\<close>
+ML_val \<open>
   map (fn test => check_upto test 0 3) testers
-*}
-ML_val {* 
+\<close>
+ML_val \<open>
   map (fn test => check_upto test 0 7) testers
-*}
+\<close>
 
-text {* Note that all conjectures must be executable to obtain the testers with the function above. *}
+text \<open>Note that all conjectures must be executable to obtain the testers with the function above.\<close>
 
 
 end