changeset 39915 | ecf97cf3d248 |
parent 39727 | 5dab9549c80d |
child 40122 | 1d8ad2ff3e01 |
--- a/src/HOL/Library/Dlist.thy Sat Oct 02 12:32:31 2010 +0200 +++ b/src/HOL/Library/Dlist.thy Mon Oct 04 12:22:58 2010 +0200 @@ -140,7 +140,7 @@ case (Abs_dlist xs) then have "distinct xs" and dxs: "dxs = Dlist xs" by (simp_all add: Dlist_def distinct_remdups_id) from `distinct xs` have "P (Dlist xs)" - proof (induct xs rule: distinct_induct) + proof (induct xs) case Nil from empty show ?case by (simp add: empty_def) next case (insert x xs)