| changeset 11701 | 3d51fbf81c17 |
| parent 9556 | dcdcfb0545e0 |
| child 11704 | 3c50a2cd6f00 |
--- a/src/HOL/IMP/Examples.ML Fri Oct 05 21:50:37 2001 +0200 +++ b/src/HOL/IMP/Examples.ML Fri Oct 05 21:52:39 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:=#0)"; +\ <factorial a b, Mem(a:=# 3)> -c-> Mem(b:=# 6,a:=Numeral0)"; by (ftac not_sym 1); by step; by step;