src/HOLCF/IOA/ABP/Lemmas.ML
changeset 13524 604d0f3622d6
parent 12218 6597093b77e7
child 14401 477380c74c1d
     1.1 --- a/src/HOLCF/IOA/ABP/Lemmas.ML	Tue Aug 27 11:03:02 2002 +0200
     1.2 +++ b/src/HOLCF/IOA/ABP/Lemmas.ML	Tue Aug 27 11:03:05 2002 +0200
     1.3 @@ -6,10 +6,6 @@
     1.4  
     1.5  (* Logic *)
     1.6  
     1.7 -val prems = goal HOL.thy "(P ==> Q-->R) ==> P&Q --> R";
     1.8 -  by (fast_tac (claset() addDs prems) 1);
     1.9 -qed "imp_conj_lemma";
    1.10 -
    1.11  goal HOL.thy "(~(A&B)) = ((~A)&B| ~B)";
    1.12  by (Fast_tac 1);
    1.13  val and_de_morgan_and_absorbe = result();