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