changeset 24853 | aab5798e5a33 |
parent 18556 | dc39832e9280 |
child 26825 | 0373ed6f04b1 |
--- a/src/HOL/UNITY/Simple/Reach.thy Thu Oct 04 21:11:06 2007 +0200 +++ b/src/HOL/UNITY/Simple/Reach.thy Fri Oct 05 08:38:09 2007 +0200 @@ -121,7 +121,7 @@ apply (unfold metric_def) apply (subgoal_tac "{v. ~ (s (x:=True)) v} = {v. ~ s v} - {x}") prefer 2 apply force -apply (simp add: card_Suc_Diff1) +apply (simp add: card_Suc_Diff1 del:card_Diff_insert) done lemma metric_less [intro!]: "~ s x ==> metric (s(x:=True)) < metric s"