src/HOL/Predicate_Compile_Examples/Context_Free_Grammar_Example.thy
changeset 39463 7ce0ed8dc4d6
parent 39189 d183bf90dabd
child 39800 17e29ddd538e
     1.1 --- a/src/HOL/Predicate_Compile_Examples/Context_Free_Grammar_Example.thy	Thu Sep 16 13:49:06 2010 +0200
     1.2 +++ b/src/HOL/Predicate_Compile_Examples/Context_Free_Grammar_Example.thy	Thu Sep 16 13:49:08 2010 +0200
     1.3 @@ -19,7 +19,7 @@
     1.4  declare size_list_def[symmetric, code_pred_inline]
     1.5  
     1.6  
     1.7 -setup {* Quickcheck.add_generator ("prolog", Code_Prolog.quickcheck) *}
     1.8 +setup {* Context.theory_map (Quickcheck.add_generator ("prolog", Code_Prolog.quickcheck)) *}
     1.9  
    1.10  datatype alphabet = a | b
    1.11  
    1.12 @@ -61,9 +61,7 @@
    1.13    limited_types = [],
    1.14    limited_predicates = [(["s1", "a1", "b1"], 2)],
    1.15    replacing = [(("s1", "limited_s1"), "quickcheck")],
    1.16 -  manual_reorder = [(("quickcheck", 1), [0,2,1,4,3,5])],
    1.17 -  timeout = Time.fromSeconds 10,
    1.18 -  prolog_system = Code_Prolog.SWI_PROLOG}) *}
    1.19 +  manual_reorder = [(("quickcheck", 1), [0,2,1,4,3,5])]}) *}
    1.20  
    1.21  
    1.22  theorem S\<^isub>1_sound:
    1.23 @@ -86,9 +84,7 @@
    1.24    limited_types = [],
    1.25    limited_predicates = [(["s2", "a2", "b2"], 3)],
    1.26    replacing = [(("s2", "limited_s2"), "quickcheck")],
    1.27 -  manual_reorder = [(("quickcheck", 1), [0,2,1,4,3,5])],
    1.28 -  timeout = Time.fromSeconds 10,
    1.29 -  prolog_system = Code_Prolog.SWI_PROLOG}) *}
    1.30 +  manual_reorder = [(("quickcheck", 1), [0,2,1,4,3,5])]}) *}
    1.31  
    1.32  
    1.33  theorem S\<^isub>2_sound:
    1.34 @@ -110,9 +106,7 @@
    1.35    limited_types = [],
    1.36    limited_predicates = [(["s3", "a3", "b3"], 6)],
    1.37    replacing = [(("s3", "limited_s3"), "quickcheck")],
    1.38 -  manual_reorder = [(("quickcheck", 1), [0,2,1,4,3,5])],
    1.39 -  timeout = Time.fromSeconds 10,
    1.40 -  prolog_system = Code_Prolog.SWI_PROLOG}) *}
    1.41 +  manual_reorder = [(("quickcheck", 1), [0,2,1,4,3,5])]}) *}
    1.42  
    1.43  lemma S\<^isub>3_sound:
    1.44  "w \<in> S\<^isub>3 \<longrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b]"
    1.45 @@ -152,9 +146,7 @@
    1.46    limited_types = [],
    1.47    limited_predicates = [(["s4", "a4", "b4"], 6)],
    1.48    replacing = [(("s4", "limited_s4"), "quickcheck")],
    1.49 -  manual_reorder = [(("quickcheck", 1), [0,2,1,4,3,5])],
    1.50 -  timeout = Time.fromSeconds 10,
    1.51 -  prolog_system = Code_Prolog.SWI_PROLOG}) *}
    1.52 +  manual_reorder = [(("quickcheck", 1), [0,2,1,4,3,5])]}) *}
    1.53  
    1.54  
    1.55  theorem S\<^isub>4_sound: