| changeset 31641 | feea4d3d743d |
| parent 31203 | 5c8fb4fd67e0 |
| child 31666 | 760c612ad800 |
| child 31706 | 1db0c8f235fb |
--- a/src/HOL/RealDef.thy Mon Jun 15 11:01:18 2009 +0200 +++ b/src/HOL/RealDef.thy Mon Jun 15 16:13:03 2009 +0200 @@ -1137,7 +1137,7 @@ begin definition - "random i = random i o\<rightarrow> (\<lambda>r. Pair (valterm_ratreal r))" + "Quickcheck.random i = Quickcheck.random i o\<rightarrow> (\<lambda>r. Pair (valterm_ratreal r))" instance ..