src/HOL/Option.ML

For each datatype `t' there is now a theorem `split_t_case' of the form

P(t_case f1 ... fn x) = ((!y1 ... ym1. x = C1 y1 ... ym1 --> P(f1 y1 ... ym1))&
...
(!y1 ... ymn. x = Cn y1 ... ymn --> P(f1 y1 ... ymn)))

The simplifier now reduces !x. (..x.. & x = t & ..x..) --> P x
to (..t.. & ..t..) --> P t
(and similarly for t=x).

(*  Title:      Option.ML
    ID:         $Id$
    Author:     Tobias Nipkow
    Copyright   1996  TU Muenchen

Derived rules
*)

val expand_option_case = split_option_case;