changeset 927 | 305e7cfda869 |
parent 0 | a5a9c433f639 |
--- a/src/Provers/genelim.ML Fri Mar 03 12:34:57 1995 +0100 +++ b/src/Provers/genelim.ML Fri Mar 03 12:48:06 1995 +0100 @@ -1,7 +1,7 @@ (** Generalized elimination rules **) (*Generalized elimination for two conclusions*) -val prems = goal pure_thy +val prems = goal proto_pure_thy "[| PROP U ==> PROP VA; \ \ PROP U ==> PROP VB; \ \ PROP U; \