# HG changeset patch
# User wenzelm
# Date 1003870615 -7200
# Node ID d1b341c3aabca354333df40b52f7f2d445962d1b
# Parent  6533ceee4cd70c804020e8e3f38946a4b2229a0e
eliminated Numeral0;

diff -r 6533ceee4cd7 -r d1b341c3aabc src/HOL/IMP/Examples.ML
--- 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;