IOA/meta_theory/Option.thy
changeset 168 44ff2275d44f
parent 156 fd1be45b64bf
equal deleted inserted replaced
167:37a6e2f55230 168:44ff2275d44f
       
     1 (*  Title:      Option.thy
       
     2     ID:         $Id$
       
     3     Author:     Tobias Nipkow
       
     4     Copyright   1994  TU Muenchen
       
     5 
       
     6 Datatype 'a option
       
     7 *)
       
     8 
     1 Option = Arith +
     9 Option = Arith +
     2 datatype 'a option = None | Some('a)
    10 datatype 'a option = None | Some('a)
     3 end
    11 end