src/HOL/Datatype.thy
changeset 22632 59c117a0bcf3
parent 22424 8a5412121687
child 22744 5cbe966d67a2
     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