# HG changeset patch
# User bulwahn
# Date 1283853113 -7200
# Node ID d183bf90dabd1e37090ac2fdab8231d6542de76c
# Parent  cd6558ed65d7cb936ca9da30ba379c4f3026b5f3
adapting example files

diff -r cd6558ed65d7 -r d183bf90dabd src/HOL/Predicate_Compile_Examples/Code_Prolog_Examples.thy
--- a/src/HOL/Predicate_Compile_Examples/Code_Prolog_Examples.thy	Tue Sep 07 11:51:53 2010 +0200
+++ b/src/HOL/Predicate_Compile_Examples/Code_Prolog_Examples.thy	Tue Sep 07 11:51:53 2010 +0200
@@ -16,6 +16,7 @@
    limited_predicates = [],
    replacing = [],
    manual_reorder = [],
+   timeout = Time.fromSeconds 10,
    prolog_system = Code_Prolog.SWI_PROLOG}) *}
 
 values "{(x, y, z). append x y z}"
@@ -28,6 +29,7 @@
    limited_predicates = [],
    replacing = [],
    manual_reorder = [],
+   timeout = Time.fromSeconds 10,
    prolog_system = Code_Prolog.YAP}) *}
 
 values "{(x, y, z). append x y z}"
@@ -38,6 +40,7 @@
    limited_predicates = [],
    replacing = [],
    manual_reorder = [],
+   timeout = Time.fromSeconds 10,
    prolog_system = Code_Prolog.SWI_PROLOG}) *}
 
 
@@ -207,6 +210,7 @@
    limited_predicates = [],
    replacing = [],
    manual_reorder = [], 
+   timeout = Time.fromSeconds 10,
    prolog_system = Code_Prolog.SWI_PROLOG}) *}
 
 values 2 "{y. notB y}"
diff -r cd6558ed65d7 -r d183bf90dabd src/HOL/Predicate_Compile_Examples/Context_Free_Grammar_Example.thy
--- a/src/HOL/Predicate_Compile_Examples/Context_Free_Grammar_Example.thy	Tue Sep 07 11:51:53 2010 +0200
+++ b/src/HOL/Predicate_Compile_Examples/Context_Free_Grammar_Example.thy	Tue Sep 07 11:51:53 2010 +0200
@@ -62,6 +62,7 @@
   limited_predicates = [(["s1", "a1", "b1"], 2)],
   replacing = [(("s1", "limited_s1"), "quickcheck")],
   manual_reorder = [(("quickcheck", 1), [0,2,1,4,3,5])],
+  timeout = Time.fromSeconds 10,
   prolog_system = Code_Prolog.SWI_PROLOG}) *}
 
 
@@ -86,6 +87,7 @@
   limited_predicates = [(["s2", "a2", "b2"], 3)],
   replacing = [(("s2", "limited_s2"), "quickcheck")],
   manual_reorder = [(("quickcheck", 1), [0,2,1,4,3,5])],
+  timeout = Time.fromSeconds 10,
   prolog_system = Code_Prolog.SWI_PROLOG}) *}
 
 
@@ -109,6 +111,7 @@
   limited_predicates = [(["s3", "a3", "b3"], 6)],
   replacing = [(("s3", "limited_s3"), "quickcheck")],
   manual_reorder = [(("quickcheck", 1), [0,2,1,4,3,5])],
+  timeout = Time.fromSeconds 10,
   prolog_system = Code_Prolog.SWI_PROLOG}) *}
 
 lemma S\<^isub>3_sound:
@@ -124,6 +127,7 @@
   limited_predicates = [],
   replacing = [],
   manual_reorder = [],
+  timeout = Time.fromSeconds 10,
   prolog_system = Code_Prolog.SWI_PROLOG}) *}
 
 
@@ -149,6 +153,7 @@
   limited_predicates = [(["s4", "a4", "b4"], 6)],
   replacing = [(("s4", "limited_s4"), "quickcheck")],
   manual_reorder = [(("quickcheck", 1), [0,2,1,4,3,5])],
+  timeout = Time.fromSeconds 10,
   prolog_system = Code_Prolog.SWI_PROLOG}) *}
 
 
diff -r cd6558ed65d7 -r d183bf90dabd src/HOL/Predicate_Compile_Examples/Hotel_Example.thy
--- a/src/HOL/Predicate_Compile_Examples/Hotel_Example.thy	Tue Sep 07 11:51:53 2010 +0200
+++ b/src/HOL/Predicate_Compile_Examples/Hotel_Example.thy	Tue Sep 07 11:51:53 2010 +0200
@@ -90,6 +90,7 @@
   limited_predicates = [],
   replacing = [],
   manual_reorder = [],
+  timeout = Time.fromSeconds 10,
   prolog_system = Code_Prolog.SWI_PROLOG}) *}
 
 values 40 "{s. hotel s}"
@@ -119,6 +120,7 @@
    limited_predicates = [(["hotel"], 5)],
    replacing = [(("hotel", "limited_hotel"), "quickcheck")],
    manual_reorder = [],
+   timeout = Time.fromSeconds 10,
    prolog_system = Code_Prolog.SWI_PROLOG}) *}
 
 lemma
diff -r cd6558ed65d7 -r d183bf90dabd src/HOL/Predicate_Compile_Examples/Lambda_Example.thy
--- a/src/HOL/Predicate_Compile_Examples/Lambda_Example.thy	Tue Sep 07 11:51:53 2010 +0200
+++ b/src/HOL/Predicate_Compile_Examples/Lambda_Example.thy	Tue Sep 07 11:51:53 2010 +0200
@@ -88,6 +88,7 @@
     replacing = [(("typing", "limited_typing"), "quickcheck"),
                  (("nthel1", "limited_nthel1"), "lim_typing")],
     manual_reorder = [],
+    timeout = Time.fromSeconds 10,
     prolog_system = Code_Prolog.SWI_PROLOG}) *}
 
 lemma
diff -r cd6558ed65d7 -r d183bf90dabd src/HOL/Predicate_Compile_Examples/List_Examples.thy
--- a/src/HOL/Predicate_Compile_Examples/List_Examples.thy	Tue Sep 07 11:51:53 2010 +0200
+++ b/src/HOL/Predicate_Compile_Examples/List_Examples.thy	Tue Sep 07 11:51:53 2010 +0200
@@ -13,6 +13,7 @@
       (("revP", "limited_revP"), "quickcheck"),
       (("appendP", "limited_appendP"), "lim_revP")],
    manual_reorder = [],
+   timeout = Time.fromSeconds 10,
    prolog_system = Code_Prolog.SWI_PROLOG}) *}
 
 lemma "(xs :: nat list) = ys @ ys --> rev xs = xs"
diff -r cd6558ed65d7 -r d183bf90dabd src/HOL/Predicate_Compile_Examples/Reg_Exp_Example.thy
--- a/src/HOL/Predicate_Compile_Examples/Reg_Exp_Example.thy	Tue Sep 07 11:51:53 2010 +0200
+++ b/src/HOL/Predicate_Compile_Examples/Reg_Exp_Example.thy	Tue Sep 07 11:51:53 2010 +0200
@@ -1,4 +1,4 @@
-theory RegExp_Example
+theory Reg_Exp_Example
 imports Predicate_Compile_Quickcheck Code_Prolog
 begin
 
@@ -158,7 +158,7 @@
   assumes "q = Seq (Sym N0) (Sym N0)"
   assumes "s = [N0, N0]"
   shows "accepts (And (repInt n k p) (repInt n k q)) s --> accepts (repInt n k (And p q)) s"
-quickcheck[generator = predicate_compile_wo_ff, iterations = 1, expect = counterexample]
+(*quickcheck[generator = predicate_compile_wo_ff, iterations = 1, expect = counterexample]*)
 quickcheck[generator = prolog, iterations = 1, size = 1, expect = counterexample]
 oops