diff -r 65abf447151b -r 390c9fb786b5 src/FOL/FOL.ML
--- a/src/FOL/FOL.ML	Fri Jan 31 17:50:47 1997 +0100
+++ b/src/FOL/FOL.ML	Fri Jan 31 17:51:42 1997 +0100
@@ -9,6 +9,8 @@
 open FOL;
 
 
+val ccontr = FalseE RS classical;
+
 (*** Classical introduction rules for | and EX ***)
 
 qed_goal "disjCI" FOL.thy