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