adapting two examples in Predicate_Compile_Examples
authorbulwahn
Thu, 21 Jul 2011 08:31:35 +0200
changeset 44808768c70befd59
parent 44807 127749bbc639
child 44809 78a0a2ad91a3
adapting two examples in Predicate_Compile_Examples
src/HOL/Predicate_Compile_Examples/Lambda_Example.thy
src/HOL/Predicate_Compile_Examples/List_Examples.thy
     1.1 --- a/src/HOL/Predicate_Compile_Examples/Lambda_Example.thy	Wed Jul 20 23:47:27 2011 +0200
     1.2 +++ b/src/HOL/Predicate_Compile_Examples/Lambda_Example.thy	Thu Jul 21 08:31:35 2011 +0200
     1.3 @@ -79,7 +79,7 @@
     1.4  
     1.5  section {* Manual setup to find counterexample *}
     1.6  
     1.7 -setup {* Context.theory_map (Quickcheck.add_generator ("prolog", Code_Prolog.quickcheck)) *}
     1.8 +setup {* Context.theory_map (Quickcheck.add_tester ("prolog", (Code_Prolog.active, Code_Prolog.test_goals))) *}
     1.9  
    1.10  setup {* Code_Prolog.map_code_options (K 
    1.11    { ensure_groundness = true,
     2.1 --- a/src/HOL/Predicate_Compile_Examples/List_Examples.thy	Wed Jul 20 23:47:27 2011 +0200
     2.2 +++ b/src/HOL/Predicate_Compile_Examples/List_Examples.thy	Thu Jul 21 08:31:35 2011 +0200
     2.3 @@ -5,7 +5,7 @@
     2.4    "~~/src/HOL/Library/Code_Prolog"
     2.5  begin
     2.6  
     2.7 -setup {* Context.theory_map (Quickcheck.add_generator ("prolog", Code_Prolog.quickcheck)) *}
     2.8 +setup {* Context.theory_map (Quickcheck.add_tester ("prolog", (Code_Prolog.active, Code_Prolog.test_goals))) *}
     2.9  
    2.10  setup {* Code_Prolog.map_code_options (K 
    2.11    {ensure_groundness = true,