src/HOL/ex/CodeEmbed.thy
changeset 21912 ff45788e7bf9
parent 21757 093ca3efb132
     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;