src/HOL/Option.thy
changeset 57123 b5324647e0f1
parent 57091 1fa9c19ba2c9
child 58112 8081087096ad
     1.1 --- a/src/HOL/Option.thy	Fri May 30 12:27:51 2014 +0200
     1.2 +++ b/src/HOL/Option.thy	Fri May 30 12:27:51 2014 +0200
     1.3 @@ -11,6 +11,7 @@
     1.4  datatype_new 'a option =
     1.5      None
     1.6    | Some (the: 'a)
     1.7 +
     1.8  datatype_compat option
     1.9  
    1.10  lemma [case_names None Some, cases type: option]: