# HG changeset patch # User haftmann # Date 1318769280 -7200 # Node ID e877b76c72bdaa285762542da823dfbec8c4542c # Parent 2dd44cd8f9633342e4097ffff9a7d048133c1ca2 hide not_member as also member diff -r 2dd44cd8f963 -r e877b76c72bd src/HOL/Set.thy --- a/src/HOL/Set.thy Sat Oct 15 20:40:13 2011 +0200 +++ b/src/HOL/Set.thy Sun Oct 16 14:48:00 2011 +0200 @@ -1764,7 +1764,7 @@ lemma vimage_code [code]: "(f -` A) x = A (f x)" by (simp add: vimage_def Collect_def mem_def) -hide_const (open) member +hide_const (open) member not_member text {* Misc theorem and ML bindings *}