# HG changeset patch
# User haftmann
# Date 1167243003 -3600
# Node ID ff45788e7bf9c3ce5ab4dcab1dd5a38dd7990a9c
# Parent  e29bcab0c81c8ded57c86974e9fc5ac4d0b0e56d
dropped section header

diff -r e29bcab0c81c -r ff45788e7bf9 src/HOL/ex/CodeEmbed.thy
--- 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;
diff -r e29bcab0c81c -r ff45788e7bf9 src/HOL/ex/CodeRandom.thy
--- 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"