dropped section header
authorhaftmann
Wed Dec 27 19:10:03 2006 +0100 (2006-12-27)
changeset 21912ff45788e7bf9
parent 21911 e29bcab0c81c
child 21913 1224048fb8f9
dropped section header
src/HOL/ex/CodeEmbed.thy
src/HOL/ex/CodeRandom.thy
     1.1 --- a/src/HOL/ex/CodeEmbed.thy	Wed Dec 27 19:10:00 2006 +0100
     1.2 +++ b/src/HOL/ex/CodeEmbed.thy	Wed Dec 27 19:10:03 2006 +0100
     1.3 @@ -8,9 +8,6 @@
     1.4  imports Main MLString
     1.5  begin
     1.6  
     1.7 -section {* Embedding (a subset of) the Pure term algebra in HOL *}
     1.8 -
     1.9 -
    1.10  subsection {* Definitions *}
    1.11  
    1.12  types vname = ml_string;
     2.1 --- a/src/HOL/ex/CodeRandom.thy	Wed Dec 27 19:10:00 2006 +0100
     2.2 +++ b/src/HOL/ex/CodeRandom.thy	Wed Dec 27 19:10:03 2006 +0100
     2.3 @@ -8,8 +8,6 @@
     2.4  imports State_Monad
     2.5  begin
     2.6  
     2.7 -section {* A simple random engine *}
     2.8 -
     2.9  consts
    2.10    pick :: "(nat \<times> 'a) list \<Rightarrow> nat \<Rightarrow> 'a"
    2.11