src/HOL/ex/CodeRandom.thy
changeset 22107 926afa3361e1
parent 21912 ff45788e7bf9