src/HOL/Option.ML
changeset 4071 4747aefbbc52
parent 4032 4b1c69d8b767
child 4133 0a08c2b9b1ed
equal deleted inserted replaced
4070:3a6e1e562aed 4071:4747aefbbc52
     3     Author:     Tobias Nipkow
     3     Author:     Tobias Nipkow
     4     Copyright   1996  TU Muenchen
     4     Copyright   1996  TU Muenchen
     5 
     5 
     6 Derived rules
     6 Derived rules
     7 *)
     7 *)
     8 
       
     9 val expand_option_case = split_option_case;