src/HOL/Option.thy
changeset 57091 1fa9c19ba2c9
parent 55867 79b915f26533
child 57123 b5324647e0f1
     1.1 --- a/src/HOL/Option.thy	Mon May 26 16:32:51 2014 +0200
     1.2 +++ b/src/HOL/Option.thy	Mon May 26 16:32:55 2014 +0200
     1.3 @@ -9,7 +9,7 @@
     1.4  begin
     1.5  
     1.6  datatype_new 'a option =
     1.7 -    =: None
     1.8 +    None
     1.9    | Some (the: 'a)
    1.10  datatype_compat option
    1.11