src/HOL/HOL.ML
changeset 1334 32a9fde85699
parent 923 ff1574a81019
child 1338 d2fc3bfaee7f
     1.1 --- a/src/HOL/HOL.ML	Thu Nov 16 12:18:38 1995 +0100
     1.2 +++ b/src/HOL/HOL.ML	Thu Nov 16 19:50:40 1995 +0100
     1.3 @@ -126,8 +126,12 @@
     1.4    [ (rtac (major RS notE RS notI) 1), 
     1.5      (etac minor 1) ]);
     1.6  
     1.7 +qed_goal "rev_contrapos" HOL.thy "[| P==>Q; ~Q |] ==> ~P"
     1.8 + (fn [major,minor]=> 
     1.9 +  [ (rtac (minor RS contrapos) 1), (etac major 1) ]);
    1.10 +
    1.11  (* ~(?t = ?s) ==> ~(?s = ?t) *)
    1.12 -val [not_sym] = compose(sym,2,contrapos);
    1.13 +bind_thm("not_sym", sym COMP rev_contrapos);
    1.14  
    1.15  
    1.16  (** Existential quantifier **)