# HG changeset patch # User oheimb # Date 884279181 -3600 # Node ID 006e5572aca8654048c9112f2359bb38227da22b # Parent 20a7fddb706a0b2354b8c48a55b56ab7df2b6c59 *** empty log message *** diff -r 20a7fddb706a -r 006e5572aca8 src/HOLCF/IOA/NTP/Lemmas.ML --- 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";