| changeset 43887 | 442aceb54969 |
| parent 43733 | a6ca7b83612f |
| child 44278 | 1220ecb81e8f |
--- 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