src/Provers/genelim.ML
changeset 927 305e7cfda869
parent 0 a5a9c433f639
equal deleted inserted replaced
926:9d1348498c36 927:305e7cfda869
     1 (** Generalized elimination rules **)
     1 (** Generalized elimination rules **)
     2 
     2 
     3 (*Generalized elimination for two conclusions*)
     3 (*Generalized elimination for two conclusions*)
     4 val prems = goal pure_thy 
     4 val prems = goal proto_pure_thy 
     5      "[| PROP U ==> PROP VA;  \
     5      "[| PROP U ==> PROP VA;  \
     6 \        PROP U ==> PROP VB;  \
     6 \        PROP U ==> PROP VB;  \
     7 \        PROP U;              \
     7 \        PROP U;              \
     8 \        [| PROP VA; PROP VB |] ==> PROP W    \
     8 \        [| PROP VA; PROP VB |] ==> PROP W    \
     9 \     |] ==> PROP W";
     9 \     |] ==> PROP W";