equal
deleted
inserted
replaced
108 \ a:=a-1 \ |
108 \ a:=a-1 \ |
109 \ END \ |
109 \ END \ |
110 \ {b = fac A}"; |
110 \ {b = fac A}"; |
111 |
111 |
112 by (hoare_tac 1); |
112 by (hoare_tac 1); |
113 |
|
114 by (safe_tac HOL_cs); |
113 by (safe_tac HOL_cs); |
115 |
|
116 by (res_inst_tac [("n","a")] natE 1); |
114 by (res_inst_tac [("n","a")] natE 1); |
117 by (ALLGOALS (asm_simp_tac (!simpset addsimps [mult_assoc]))); |
115 by (ALLGOALS |
|
116 (asm_simp_tac |
|
117 (!simpset addsimps [add_mult_distrib,add_mult_distrib2,mult_assoc]))); |
118 by (fast_tac HOL_cs 1); |
118 by (fast_tac HOL_cs 1); |
119 |
119 |
120 qed"factorial"; |
120 qed"factorial"; |