Declaration of ccontr (classical contradiction) for HOL compatibility
authorpaulson
Fri Jan 31 17:51:42 1997 +0100 (1997-01-31)
changeset 2576390c9fb786b5
parent 2575 65abf447151b
child 2577 eec6bdf53809
Declaration of ccontr (classical contradiction) for HOL compatibility
src/FOL/FOL.ML
     1.1 --- a/src/FOL/FOL.ML	Fri Jan 31 17:50:47 1997 +0100
     1.2 +++ b/src/FOL/FOL.ML	Fri Jan 31 17:51:42 1997 +0100
     1.3 @@ -9,6 +9,8 @@
     1.4  open FOL;
     1.5  
     1.6  
     1.7 +val ccontr = FalseE RS classical;
     1.8 +
     1.9  (*** Classical introduction rules for | and EX ***)
    1.10  
    1.11  qed_goal "disjCI" FOL.thy