--- a/src/HOL/Quickcheck_Benchmark/Needham_Schroeder_Base.thy Wed Oct 29 11:13:24 2014 +0100
+++ b/src/HOL/Quickcheck_Benchmark/Needham_Schroeder_Base.thy Wed Oct 29 11:19:27 2014 +0100
@@ -194,7 +194,7 @@
declare ListMem_iff[symmetric, code_pred_inline]
declare [[quickcheck_timing]]
-setup {* Exhaustive_Generators.setup_exhaustive_datatype_interpretation *}
+setup Exhaustive_Generators.setup_exhaustive_datatype_interpretation
declare [[quickcheck_full_support = false]]
end
\ No newline at end of file
--- a/src/HOL/Quickcheck_Examples/Completeness.thy Wed Oct 29 11:13:24 2014 +0100
+++ b/src/HOL/Quickcheck_Examples/Completeness.thy Wed Oct 29 11:19:27 2014 +0100
@@ -20,7 +20,7 @@
"is_some x \<longleftrightarrow> x \<noteq> None"
by (cases x) simp_all
-setup {* Exhaustive_Generators.setup_exhaustive_datatype_interpretation *}
+setup Exhaustive_Generators.setup_exhaustive_datatype_interpretation
subsection {* Defining the size of values *}
--- a/src/HOL/Quickcheck_Examples/Quickcheck_Examples.thy Wed Oct 29 11:13:24 2014 +0100
+++ b/src/HOL/Quickcheck_Examples/Quickcheck_Examples.thy Wed Oct 29 11:19:27 2014 +0100
@@ -544,7 +544,7 @@
text {* with the simple testing scheme *}
-setup {* Exhaustive_Generators.setup_exhaustive_datatype_interpretation *}
+setup Exhaustive_Generators.setup_exhaustive_datatype_interpretation
declare [[quickcheck_full_support = false]]
lemma
--- a/src/HOL/Quickcheck_Examples/Quickcheck_Interfaces.thy Wed Oct 29 11:13:24 2014 +0100
+++ b/src/HOL/Quickcheck_Examples/Quickcheck_Interfaces.thy Wed Oct 29 11:19:27 2014 +0100
@@ -11,7 +11,7 @@
First, this requires to setup special generators for all datatypes via the following command.
*}
-setup {* Exhaustive_Generators.setup_bounded_forall_datatype_interpretation *}
+setup Exhaustive_Generators.setup_bounded_forall_datatype_interpretation
text {*
Now, the function Quickcheck.mk_batch_validator : Proof.context -> term list -> (int -> bool) list option
--- a/src/HOL/Quickcheck_Exhaustive.thy Wed Oct 29 11:13:24 2014 +0100
+++ b/src/HOL/Quickcheck_Exhaustive.thy Wed Oct 29 11:19:27 2014 +0100
@@ -618,7 +618,7 @@
ML_file "Tools/Quickcheck/exhaustive_generators.ML"
-setup {* Exhaustive_Generators.setup *}
+setup Exhaustive_Generators.setup
declare [[quickcheck_batch_tester = exhaustive]]
--- a/src/HOL/Quickcheck_Narrowing.thy Wed Oct 29 11:13:24 2014 +0100
+++ b/src/HOL/Quickcheck_Narrowing.thy Wed Oct 29 11:19:27 2014 +0100
@@ -197,7 +197,7 @@
ML_file "Tools/Quickcheck/narrowing_generators.ML"
-setup {* Narrowing_Generators.setup *}
+setup Narrowing_Generators.setup
definition narrowing_dummy_partial_term_of :: "('a :: partial_term_of) itself => narrowing_term => term"
where