List.ML

 by (etac Abs_List_inverse 1);
 val inj_onto_Abs_List = result();
 
 (** Distinctness of constructors **)
 
-goalw List.thy [NIL_def,CONS_def] "~ CONS(M,N) = NIL";
+goalw List.thy [NIL_def,CONS_def] "CONS(M,N) ~= NIL";
 by (rtac In1_not_In0 1);
 val CONS_not_NIL = result();
 val NIL_not_CONS = standard (CONS_not_NIL RS not_sym);
 
 val CONS_neq_NIL = standard (CONS_not_NIL RS notE);
 val NIL_neq_CONS = sym RS CONS_neq_NIL;
 
-goalw List.thy [Nil_def,Cons_def] "~ Cons(x,xs) = Nil";
+goalw List.thy [Nil_def,Cons_def] "Cons(x,xs) ~= Nil";
 by (rtac (CONS_not_NIL RS (inj_onto_Abs_List RS inj_onto_contraD)) 1);
 by (REPEAT (resolve_tac [rangeI, NIL_I, CONS_I, Rep_List] 1));
 val Cons_not_Nil = result();
 
 val Nil_not_Cons = standard (Cons_not_Nil RS not_sym);

 val list_free_simps = [Cons_not_Nil, Nil_not_Cons, Cons_Cons_eq,
 		       CONS_not_NIL, NIL_not_CONS, CONS_CONS_eq,
 		       NIL_I, CONS_I];
 val list_free_ss = HOL_ss  addsimps  list_free_simps;
 
-goal List.thy "!!N. N: List(A) ==> !M. ~ N = CONS(M,N)";
+goal List.thy "!!N. N: List(A) ==> !M. N ~= CONS(M,N)";
 by (etac List_induct 1);
 by (ALLGOALS (asm_simp_tac list_free_ss));
 val not_CONS_self = result();
 
-goal List.thy "!x. ~ l=Cons(x,l)";
+goal List.thy "!x. l ~= Cons(x,l)";
 by (list_ind_tac "l" 1);
 by (ALLGOALS (asm_simp_tac list_free_ss));
 val not_Cons_self = result();