| changeset 52847 | 820339715ffe |
| parent 46226 | e88e980ed735 |
| child 58860 | fee7cfa69c50 |
--- a/src/HOL/MicroJava/DFA/Kildall.thy Fri Aug 02 11:51:21 2013 +0200 +++ b/src/HOL/MicroJava/DFA/Kildall.thy Fri Aug 02 12:17:55 2013 +0200 @@ -67,9 +67,8 @@ (** merges **) -lemma length_merges [rule_format, simp]: - "\<forall>ss. size(merges f ps ss) = size ss" - by (induct_tac ps, auto) +lemma length_merges [simp]: "size(merges f ps ss) = size ss" + by (induct ps arbitrary: ss) auto lemma (in Semilat) merges_preserves_type_lemma: