tuned;
authorwenzelm
Wed Oct 29 11:19:27 2014 +0100 (2014-10-29)
changeset 58813625d04d4fd2a
parent 58812 5a9a2d3b9f8b
child 58814 4c0ad4162cb7
tuned;
src/HOL/Quickcheck_Benchmark/Needham_Schroeder_Base.thy
src/HOL/Quickcheck_Examples/Completeness.thy
src/HOL/Quickcheck_Examples/Quickcheck_Examples.thy
src/HOL/Quickcheck_Examples/Quickcheck_Interfaces.thy
src/HOL/Quickcheck_Exhaustive.thy
src/HOL/Quickcheck_Narrowing.thy
     1.1 --- a/src/HOL/Quickcheck_Benchmark/Needham_Schroeder_Base.thy	Wed Oct 29 11:13:24 2014 +0100
     1.2 +++ b/src/HOL/Quickcheck_Benchmark/Needham_Schroeder_Base.thy	Wed Oct 29 11:19:27 2014 +0100
     1.3 @@ -194,7 +194,7 @@
     1.4  declare ListMem_iff[symmetric, code_pred_inline]
     1.5  declare [[quickcheck_timing]]
     1.6  
     1.7 -setup {* Exhaustive_Generators.setup_exhaustive_datatype_interpretation *}
     1.8 +setup Exhaustive_Generators.setup_exhaustive_datatype_interpretation
     1.9  declare [[quickcheck_full_support = false]]
    1.10  
    1.11  end
    1.12 \ No newline at end of file
     2.1 --- a/src/HOL/Quickcheck_Examples/Completeness.thy	Wed Oct 29 11:13:24 2014 +0100
     2.2 +++ b/src/HOL/Quickcheck_Examples/Completeness.thy	Wed Oct 29 11:19:27 2014 +0100
     2.3 @@ -20,7 +20,7 @@
     2.4    "is_some x \<longleftrightarrow> x \<noteq> None"
     2.5    by (cases x) simp_all
     2.6  
     2.7 -setup {* Exhaustive_Generators.setup_exhaustive_datatype_interpretation *} 
     2.8 +setup Exhaustive_Generators.setup_exhaustive_datatype_interpretation
     2.9  
    2.10  subsection {* Defining the size of values *}
    2.11  
     3.1 --- a/src/HOL/Quickcheck_Examples/Quickcheck_Examples.thy	Wed Oct 29 11:13:24 2014 +0100
     3.2 +++ b/src/HOL/Quickcheck_Examples/Quickcheck_Examples.thy	Wed Oct 29 11:19:27 2014 +0100
     3.3 @@ -544,7 +544,7 @@
     3.4  
     3.5  text {* with the simple testing scheme *}
     3.6  
     3.7 -setup {* Exhaustive_Generators.setup_exhaustive_datatype_interpretation *}
     3.8 +setup Exhaustive_Generators.setup_exhaustive_datatype_interpretation
     3.9  declare [[quickcheck_full_support = false]]
    3.10  
    3.11  lemma
     4.1 --- a/src/HOL/Quickcheck_Examples/Quickcheck_Interfaces.thy	Wed Oct 29 11:13:24 2014 +0100
     4.2 +++ b/src/HOL/Quickcheck_Examples/Quickcheck_Interfaces.thy	Wed Oct 29 11:19:27 2014 +0100
     4.3 @@ -11,7 +11,7 @@
     4.4  First, this requires to setup special generators for all datatypes via the following command.
     4.5  *}
     4.6  
     4.7 -setup {* Exhaustive_Generators.setup_bounded_forall_datatype_interpretation *}
     4.8 +setup Exhaustive_Generators.setup_bounded_forall_datatype_interpretation
     4.9  
    4.10  text {*
    4.11  Now, the function Quickcheck.mk_batch_validator : Proof.context -> term list -> (int -> bool) list option
     5.1 --- a/src/HOL/Quickcheck_Exhaustive.thy	Wed Oct 29 11:13:24 2014 +0100
     5.2 +++ b/src/HOL/Quickcheck_Exhaustive.thy	Wed Oct 29 11:19:27 2014 +0100
     5.3 @@ -618,7 +618,7 @@
     5.4  
     5.5  ML_file "Tools/Quickcheck/exhaustive_generators.ML"
     5.6  
     5.7 -setup {* Exhaustive_Generators.setup *}
     5.8 +setup Exhaustive_Generators.setup
     5.9  
    5.10  declare [[quickcheck_batch_tester = exhaustive]]
    5.11  
     6.1 --- a/src/HOL/Quickcheck_Narrowing.thy	Wed Oct 29 11:13:24 2014 +0100
     6.2 +++ b/src/HOL/Quickcheck_Narrowing.thy	Wed Oct 29 11:19:27 2014 +0100
     6.3 @@ -197,7 +197,7 @@
     6.4  
     6.5  ML_file "Tools/Quickcheck/narrowing_generators.ML"
     6.6  
     6.7 -setup {* Narrowing_Generators.setup *}
     6.8 +setup Narrowing_Generators.setup
     6.9  
    6.10  definition narrowing_dummy_partial_term_of :: "('a :: partial_term_of) itself => narrowing_term => term"
    6.11  where