avoid clash with Quickcheck's generated 'random_xxx' function
authorblanchet
Wed, 17 Sep 2014 11:54:59 +0200
changeset 58357 a416218a3a11
parent 58356 2f04f1fd28aa
child 58358 cdce4471d590
avoid clash with Quickcheck's generated 'random_xxx' function
src/Doc/Datatypes/Datatypes.thy
--- a/src/Doc/Datatypes/Datatypes.thy	Wed Sep 17 11:12:46 2014 +0200
+++ b/src/Doc/Datatypes/Datatypes.thy	Wed Sep 17 11:54:59 2014 +0200
@@ -1997,7 +1997,7 @@
 pseudorandom seed (@{text n}):
 *}
 
-    primcorec
+    primcorec(*<*) (in early)(*>*)
       random_process :: "'a stream \<Rightarrow> (int \<Rightarrow> int) \<Rightarrow> int \<Rightarrow> 'a process"
     where
       "random_process s f n =