eliminated Numeral0;

--- a/src/HOL/IMP/Examples.ML	Tue Oct 23 22:54:01 2001 +0200
+++ b/src/HOL/IMP/Examples.ML	Tue Oct 23 22:56:55 2001 +0200
@@ -34,7 +34,7 @@
 val step = resolve_tac evalc.intrs 1;
 val simp = Asm_simp_tac 1;
 Goalw [factorial_def] "a~=b ==> \
-\ <factorial a b, Mem(a:=3)>  -c-> Mem(b:=6,a:=Numeral0)";
+\ <factorial a b, Mem(a:=3)>  -c-> Mem(b:=6, a:=0)";
 by (ftac not_sym 1);
 by step;
 by  step;