src/HOL/ex/CodeRandom.thy
changeset 21912 ff45788e7bf9
parent 21876 96a601bc59d8
     1.1 --- a/src/HOL/ex/CodeRandom.thy	Wed Dec 27 19:10:00 2006 +0100
     1.2 +++ b/src/HOL/ex/CodeRandom.thy	Wed Dec 27 19:10:03 2006 +0100
     1.3 @@ -8,8 +8,6 @@
     1.4  imports State_Monad
     1.5  begin
     1.6  
     1.7 -section {* A simple random engine *}
     1.8 -
     1.9  consts
    1.10    pick :: "(nat \<times> 'a) list \<Rightarrow> nat \<Rightarrow> 'a"
    1.11