author | lcp |
Fri, 03 Dec 1993 12:41:54 +0100 | |
changeset 23 | 2c7fedb2713c |
parent 22 | 17b6487e1ac7 |
child 24 | 340d21c86440 |
--- a/ex/cla.ML Wed Dec 01 13:05:25 1993 +0100 +++ b/ex/cla.ML Fri Dec 03 12:41:54 1993 +0100 @@ -139,6 +139,14 @@ by (fast_tac HOL_cs 1); result(); +(*From Wishnu Prasetya*) +goal HOL.thy + "(!s. q(s) --> r(s)) & ~r(s) & (!s. ~r(s) & ~q(s) --> p(t) | q(t)) \ +\ --> p(t) | r(t)"; +by (fast_tac HOL_cs 1); +result(); + + writeln"Problems requiring quantifier duplication"; (*Needs multiple instantiation of the quantifier.*)