# HG changeset patch
# User bulwahn
# Date 1300102449 -3600
# Node ID 27a61a3266d86424aa4a9f5944e9c7ebcffc7a0c
# Parent  fdd37cfcd4a31bd17d932bb3a741592483313a77
correcting names in Narrowing_Engine and example theory for Quickcheck_Narrowing

diff -r fdd37cfcd4a3 -r 27a61a3266d8 src/HOL/Library/Quickcheck_Narrowing.thy
--- a/src/HOL/Library/Quickcheck_Narrowing.thy	Mon Mar 14 12:34:08 2011 +0100
+++ b/src/HOL/Library/Quickcheck_Narrowing.thy	Mon Mar 14 12:34:09 2011 +0100
@@ -4,7 +4,8 @@
 
 theory Quickcheck_Narrowing
 imports Main "~~/src/HOL/Library/Code_Char"
-uses ("~~/src/HOL/Tools/Quickcheck/narrowing_generators.ML")
+uses
+  ("~~/src/HOL/Tools/Quickcheck/narrowing_generators.ML")
 begin
 
 subsection {* Counterexample generator *}
diff -r fdd37cfcd4a3 -r 27a61a3266d8 src/HOL/Tools/Quickcheck/Narrowing_Engine.hs
--- a/src/HOL/Tools/Quickcheck/Narrowing_Engine.hs	Mon Mar 14 12:34:08 2011 +0100
+++ b/src/HOL/Tools/Quickcheck/Narrowing_Engine.hs	Mon Mar 14 12:34:09 2011 +0100
@@ -89,9 +89,9 @@
   property app = P $ \n d -> Result [] [] (app . reverse);
 };
 
-instance (Term_of a, Serial a, Testable b) => Testable (a -> b) where {
+instance (Term_of a, Narrowing a, Testable b) => Testable (a -> b) where {
   property f = P $ \n d ->
-    let C t c = series d
+    let C t c = narrowing d
         c' = conv c
         r = run (\(x:xs) -> f xs (c' x)) (n+1) d
     in  r { args = Var [n] t : args r, showArgs = (show . term_of . c') : showArgs r };
diff -r fdd37cfcd4a3 -r 27a61a3266d8 src/HOL/ex/Quickcheck_Narrowing_Examples.thy
--- a/src/HOL/ex/Quickcheck_Narrowing_Examples.thy	Mon Mar 14 12:34:08 2011 +0100
+++ b/src/HOL/ex/Quickcheck_Narrowing_Examples.thy	Mon Mar 14 12:34:09 2011 +0100
@@ -115,12 +115,12 @@
                  
 subsection {* Necessary instantiation for quickcheck generator *}
 
-instantiation tree :: (serial) serial
+instantiation tree :: (narrowing) narrowing
 begin
 
-function series_tree
+function narrowing_tree
 where
-  "series_tree d = sum (cons ET) (apply (apply (apply (apply (cons MKT) series) series_tree) series_tree) series) d"
+  "narrowing_tree d = sum (cons ET) (apply (apply (apply (apply (cons MKT) narrowing) narrowing_tree) narrowing_tree) narrowing) d"
 by pat_completeness auto
 
 termination proof (relation "measure nat_of")