diff -r 17b6487e1ac7 -r 2c7fedb2713c ex/cla.ML
--- 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.*)