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