# HG changeset patch
# User bulwahn
# Date 1310978061 -7200
# Node ID 442aceb54969fe94397e9ce2837a740a11cb038b
# Parent  bf068e758783153900bee9c44e00506a57ad2c81
adding narrowing instances for real and rational

diff -r bf068e758783 -r 442aceb54969 src/HOL/Quickcheck_Narrowing.thy
--- a/src/HOL/Quickcheck_Narrowing.thy	Mon Jul 18 10:34:21 2011 +0200
+++ b/src/HOL/Quickcheck_Narrowing.thy	Mon Jul 18 10:34:21 2011 +0200
@@ -431,9 +431,8 @@
 *)
 
 hide_type code_int narrowing_type narrowing_term cons property
-hide_const int_of of_int nth error toEnum marker empty
-  C cons conv nonEmpty "apply" sum ensure_testable all exists 
-hide_const (open) Var Ctr
+hide_const int_of of_int nth error toEnum marker empty C conv nonEmpty ensure_testable all exists 
+hide_const (open) Var Ctr "apply" sum cons
 hide_fact empty_def cons_def conv.simps nonEmpty.simps apply_def sum_def ensure_testable_def all_def exists_def
 
 
diff -r bf068e758783 -r 442aceb54969 src/HOL/Rat.thy
--- a/src/HOL/Rat.thy	Mon Jul 18 10:34:21 2011 +0200
+++ b/src/HOL/Rat.thy	Mon Jul 18 10:34:21 2011 +0200
@@ -1171,6 +1171,17 @@
 
 end
 
+instantiation rat :: narrowing
+begin
+
+definition
+  "narrowing = Quickcheck_Narrowing.apply (Quickcheck_Narrowing.apply (Quickcheck_Narrowing.cons Fract) narrowing) narrowing"
+
+instance ..
+
+end
+
+
 text {* Setup for SML code generator *}
 
 types_code
diff -r bf068e758783 -r 442aceb54969 src/HOL/RealDef.thy
--- a/src/HOL/RealDef.thy	Mon Jul 18 10:34:21 2011 +0200
+++ b/src/HOL/RealDef.thy	Mon Jul 18 10:34:21 2011 +0200
@@ -1805,6 +1805,17 @@
 
 end
 
+instantiation real :: narrowing
+begin
+
+definition
+  "narrowing = Quickcheck_Narrowing.apply (Quickcheck_Narrowing.cons Ratreal) narrowing"
+
+instance ..
+
+end
+
+
 text {* Setup for SML code generator *}
 
 types_code