--- a/src/HOLCF/Holcfb.ML Thu Sep 26 12:50:48 1996 +0200
+++ b/src/HOLCF/Holcfb.ML Thu Sep 26 15:14:23 1996 +0200
@@ -18,9 +18,9 @@
(* val de_morgan2 = de_Morgan_conj RS sym; "(~a | ~b)=(~(a & b))" *)
-(* val notall2ex = not_all "(~ (!x.P(x))) = (? x.~P(x))" *)
+(* val notall2ex = not_all "(~ (!x.P(x))) = (? x.~P(x))" *)
-(* val notex2all = not_ex "(~ (? x.P(x))) = (!x.~P(x))" *)
+(* val notex2all = not_ex "(~ (? x.P(x))) = (!x.~P(x))" *)
(* val selectI3 = select_eq_Ex RS iffD2 "(? x. P(x)) ==> P(@ x.P(x))" *)