changeset 13612 | 55d32e76ef4e |
parent 13107 | 8743cc847224 |
child 16417 | 9bc16273c2d4 |
--- a/src/HOL/Induct/LFilter.thy Mon Sep 30 16:47:03 2002 +0200 +++ b/src/HOL/Induct/LFilter.thy Mon Sep 30 16:48:15 2002 +0200 @@ -125,7 +125,6 @@ lemma lfilter_eq_LNil: "lfilter p l = LNil ==> l ~: Domain(findRel p)" apply (auto iff: Domain_findRel_iff) -apply (rotate_tac 1, simp) done lemma lfilter_eq_LCons [rule_format]: