author | blanchet |
Wed, 17 Sep 2014 11:54:59 +0200 | |
changeset 58357 | a416218a3a11 |
parent 58356 | 2f04f1fd28aa |
child 58358 | cdce4471d590 |
--- 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 =