--- 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);