src/HOL/IMP/Examples.ML

 section "Factorial";
 
 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;
 by simp;
 by step;