--- a/src/HOL/ex/CodeEmbed.thy Wed Dec 27 19:10:00 2006 +0100
+++ b/src/HOL/ex/CodeEmbed.thy Wed Dec 27 19:10:03 2006 +0100
@@ -8,9 +8,6 @@
imports Main MLString
begin
-section {* Embedding (a subset of) the Pure term algebra in HOL *}
-
-
subsection {* Definitions *}
types vname = ml_string;
--- a/src/HOL/ex/CodeRandom.thy Wed Dec 27 19:10:00 2006 +0100
+++ b/src/HOL/ex/CodeRandom.thy Wed Dec 27 19:10:03 2006 +0100
@@ -8,8 +8,6 @@
imports State_Monad
begin
-section {* A simple random engine *}
-
consts
pick :: "(nat \<times> 'a) list \<Rightarrow> nat \<Rightarrow> 'a"