--- a/src/HOLCF/IOA/NTP/Lemmas.ML Thu Jan 08 18:03:36 1998 +0100
+++ b/src/HOLCF/IOA/NTP/Lemmas.ML Thu Jan 08 18:06:21 1998 +0100
@@ -6,6 +6,7 @@
*)
(* Logic *)
+
val prems = goal HOL.thy "(P ==> Q-->R) ==> P&Q --> R";
by (fast_tac (claset() addDs prems) 1);
qed "imp_conj_lemma";