src/HOL/Rat.thy
changeset 43887 442aceb54969
parent 43733 a6ca7b83612f
child 43889 90d24cafb05d
--- 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