dropped legacy ML bindings
authorhaftmann
Wed Apr 11 08:28:13 2007 +0200 (2007-04-11)
changeset 2263259c117a0bcf3
parent 22631 7ae5a6ab7bd6
child 22633 a47e4fd7ebc1
dropped legacy ML bindings
src/HOL/Datatype.thy
     1.1 --- a/src/HOL/Datatype.thy	Wed Apr 11 04:13:06 2007 +0200
     1.2 +++ b/src/HOL/Datatype.thy	Wed Apr 11 08:28:13 2007 +0200
     1.3 @@ -763,12 +763,4 @@
     1.4  code_reserved OCaml
     1.5    option None Some
     1.6  
     1.7 -
     1.8 -subsection {* Basic ML bindings *}
     1.9 -
    1.10 -ML {*
    1.11 -val not_None_eq = thm "not_None_eq";
    1.12 -val not_Some_eq = thm "not_Some_eq";
    1.13 -*}
    1.14 -
    1.15  end