diff -r d199410f1db1 -r 968d2dccf2de sum.ML
--- a/sum.ML	Mon Oct 04 15:43:54 1993 +0100
+++ b/sum.ML	Thu Oct 07 10:20:30 1993 +0100
@@ -26,14 +26,14 @@
 
 (** Distinctness of Inl and Inr **)
 
-goalw Sum.thy [Inl_Rep_def, Inr_Rep_def] "~ (Inl_Rep(a) = Inr_Rep(b))";
+goalw Sum.thy [Inl_Rep_def, Inr_Rep_def] "Inl_Rep(a) ~= Inr_Rep(b)";
 by (EVERY1 [rtac notI,
 	    etac (fun_cong RS fun_cong RS fun_cong RS iffE), 
 	    rtac (notE RS ccontr),  etac (mp RS conjunct2), 
 	    REPEAT o (ares_tac [refl,conjI]) ]);
 val Inl_Rep_not_Inr_Rep = result();
 
-goalw Sum.thy [Inl_def,Inr_def] "~ Inl(a)=Inr(b)";
+goalw Sum.thy [Inl_def,Inr_def] "Inl(a) ~= Inr(b)";
 by (rtac (inj_onto_Abs_Sum RS inj_onto_contraD) 1);
 by (rtac Inl_Rep_not_Inr_Rep 1);
 by (rtac Inl_RepI 1);