diff -r d199410f1db1 -r 968d2dccf2de Univ.ML
--- a/Univ.ML	Mon Oct 04 15:43:54 1993 +0100
+++ b/Univ.ML	Thu Oct 07 10:20:30 1993 +0100
@@ -123,7 +123,7 @@
 
 (** Scons vs Atom **)
 
-goalw Univ.thy [Atom_def,Scons_def,Push_Node_def] "~ ((M.N) = Atom(a))";
+goalw Univ.thy [Atom_def,Scons_def,Push_Node_def] "(M.N) ~= Atom(a)";
 by (rtac notI 1);
 by (etac (equalityD2 RS subsetD RS UnE) 1);
 by (rtac singletonI 1);
@@ -223,7 +223,7 @@
 
 (** Scons vs Leaf **)
 
-goalw Univ.thy [Leaf_def] "~ ((M.N) = Leaf(a))";
+goalw Univ.thy [Leaf_def] "(M.N) ~= Leaf(a)";
 by (stac o_def 1);
 by (rtac Scons_not_Atom 1);
 val Scons_not_Leaf = result();
@@ -234,7 +234,7 @@
 
 (** Scons vs Numb **)
 
-goalw Univ.thy [Numb_def] "~ ((M.N) = Numb(k))";
+goalw Univ.thy [Numb_def] "(M.N) ~= Numb(k)";
 by (stac o_def 1);
 by (rtac Scons_not_Atom 1);
 val Scons_not_Numb = result();
@@ -245,7 +245,7 @@
 
 (** Leaf vs Numb **)
 
-goalw Univ.thy [Leaf_def,Numb_def] "~ (Leaf(a) = Numb(k))";
+goalw Univ.thy [Leaf_def,Numb_def] "Leaf(a) ~= Numb(k)";
 by (simp_tac (HOL_ss addsimps [Atom_Atom_eq,Inl_not_Inr]) 1);
 val Leaf_not_Numb = result();
 val Numb_not_Leaf = standard (Leaf_not_Numb RS not_sym);
@@ -267,7 +267,7 @@
 by (etac less_zeroE 1);
 val ndepth_K0 = result();
 
-goal Univ.thy "k < Suc(LEAST x. f(x)=0) --> ~ nat_case(k, Suc(i), f) = 0";
+goal Univ.thy "k < Suc(LEAST x. f(x)=0) --> nat_case(k, Suc(i), f) ~= 0";
 by (nat_ind_tac "k" 1);
 by (ALLGOALS (simp_tac nat_ss));
 by (rtac impI 1);
@@ -393,7 +393,7 @@
 
 (** Injection **)
 
-goalw Univ.thy [In0_def,In1_def] "~ (In0(M) = In1(N))";
+goalw Univ.thy [In0_def,In1_def] "In0(M) ~= In1(N)";
 by (rtac notI 1);
 by (etac (Scons_inject1 RS Numb_inject RS Zero_neq_Suc) 1);
 val In0_not_In1 = result();