summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

src/HOL/Library/Dlist.thy

changeset 40122 | 1d8ad2ff3e01 |

parent 39915 | ecf97cf3d248 |

child 40603 | 963ee2331d20 |

1.1 --- a/src/HOL/Library/Dlist.thy Mon Oct 25 13:34:57 2010 +0200 1.2 +++ b/src/HOL/Library/Dlist.thy Mon Oct 25 13:34:58 2010 +0200 1.3 @@ -143,11 +143,11 @@ 1.4 proof (induct xs) 1.5 case Nil from empty show ?case by (simp add: empty_def) 1.6 next 1.7 - case (insert x xs) 1.8 + case (Cons x xs) 1.9 then have "\<not> member (Dlist xs) x" and "P (Dlist xs)" 1.10 by (simp_all add: member_def List.member_def) 1.11 with insrt have "P (insert x (Dlist xs))" . 1.12 - with insert show ?case by (simp add: insert_def distinct_remdups_id) 1.13 + with Cons show ?case by (simp add: insert_def distinct_remdups_id) 1.14 qed 1.15 with dxs show "P dxs" by simp 1.16 qed