| changeset 9190 | b86ff604729f |
| parent 8334 | 7896bcbd8641 |
| child 10179 | 9d5678e6bf34 |
--- a/src/HOL/UNITY/Reach.ML Thu Jun 29 12:17:18 2000 +0200 +++ b/src/HOL/UNITY/Reach.ML Thu Jun 29 12:19:27 2000 +0200 @@ -92,8 +92,8 @@ Goalw [metric_def] "~ s x ==> Suc (metric (s(x:=True))) = metric s"; by (subgoal_tac "{v. ~ (s(x:=True)) v} = {v. ~ s v} - {x}" 1); -by Auto_tac; -by (asm_simp_tac (simpset() addsimps [card_Suc_Diff1]) 1); +by (Force_tac 2); +by (asm_full_simp_tac (simpset() addsimps [card_Suc_Diff1]) 1); qed "Suc_metric"; Goal "~ s x ==> metric (s(x:=True)) < metric s";