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