src/HOL/Predicate_Compile_Examples/Context_Free_Grammar_Example.thy
changeset 39189 d183bf90dabd
parent 38962 3917c2acaec4
child 39463 7ce0ed8dc4d6
     1.1 --- a/src/HOL/Predicate_Compile_Examples/Context_Free_Grammar_Example.thy	Tue Sep 07 11:51:53 2010 +0200
     1.2 +++ b/src/HOL/Predicate_Compile_Examples/Context_Free_Grammar_Example.thy	Tue Sep 07 11:51:53 2010 +0200
     1.3 @@ -62,6 +62,7 @@
     1.4    limited_predicates = [(["s1", "a1", "b1"], 2)],
     1.5    replacing = [(("s1", "limited_s1"), "quickcheck")],
     1.6    manual_reorder = [(("quickcheck", 1), [0,2,1,4,3,5])],
     1.7 +  timeout = Time.fromSeconds 10,
     1.8    prolog_system = Code_Prolog.SWI_PROLOG}) *}
     1.9  
    1.10  
    1.11 @@ -86,6 +87,7 @@
    1.12    limited_predicates = [(["s2", "a2", "b2"], 3)],
    1.13    replacing = [(("s2", "limited_s2"), "quickcheck")],
    1.14    manual_reorder = [(("quickcheck", 1), [0,2,1,4,3,5])],
    1.15 +  timeout = Time.fromSeconds 10,
    1.16    prolog_system = Code_Prolog.SWI_PROLOG}) *}
    1.17  
    1.18  
    1.19 @@ -109,6 +111,7 @@
    1.20    limited_predicates = [(["s3", "a3", "b3"], 6)],
    1.21    replacing = [(("s3", "limited_s3"), "quickcheck")],
    1.22    manual_reorder = [(("quickcheck", 1), [0,2,1,4,3,5])],
    1.23 +  timeout = Time.fromSeconds 10,
    1.24    prolog_system = Code_Prolog.SWI_PROLOG}) *}
    1.25  
    1.26  lemma S\<^isub>3_sound:
    1.27 @@ -124,6 +127,7 @@
    1.28    limited_predicates = [],
    1.29    replacing = [],
    1.30    manual_reorder = [],
    1.31 +  timeout = Time.fromSeconds 10,
    1.32    prolog_system = Code_Prolog.SWI_PROLOG}) *}
    1.33  
    1.34  
    1.35 @@ -149,6 +153,7 @@
    1.36    limited_predicates = [(["s4", "a4", "b4"], 6)],
    1.37    replacing = [(("s4", "limited_s4"), "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  
    1.42