author | wenzelm |
Tue, 23 Oct 2001 22:56:55 +0200 | |
changeset 11912 | d1b341c3aabc |
parent 11911 | 6533ceee4cd7 |
child 11913 | 673d7bc6b9db |
--- 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;