src/FOL/FOL.ML
changeset 2576 390c9fb786b5
parent 2469 b50b8c0eec01
child 3835 9a5a4e123859
--- 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