src/HOLCF/IOA/ABP/Lemmas.ML
changeset 4423 a129b817b58a
parent 4098 71e05eb27fb6
child 4833 2e53109d4bc8
     1.1 --- a/src/HOLCF/IOA/ABP/Lemmas.ML	Tue Dec 16 15:17:26 1997 +0100
     1.2 +++ b/src/HOLCF/IOA/ABP/Lemmas.ML	Tue Dec 16 17:58:03 1997 +0100
     1.3 @@ -8,7 +8,7 @@
     1.4  (* Logic *)
     1.5  
     1.6  val prems = goal HOL.thy "(P ==> Q-->R) ==> P&Q --> R";
     1.7 -  by(fast_tac (claset() addDs prems) 1);
     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 @@ -16,7 +16,7 @@
    1.13  val and_de_morgan_and_absorbe = result();
    1.14  
    1.15  goal HOL.thy "(if C then A else B) --> (A|B)";
    1.16 -by (rtac (expand_if RS ssubst) 1);
    1.17 +by (stac expand_if 1);
    1.18  by (Fast_tac 1);
    1.19  val bool_if_impl_or = result();
    1.20