changeset 21153 | 8288c8f203de |
parent 21125 | 9b7d35ca1eef |
child 21191 | c00161fbf990 |
--- a/src/HOL/Library/ExecutableSet.thy Fri Nov 03 14:22:38 2006 +0100 +++ b/src/HOL/Library/ExecutableSet.thy Fri Nov 03 14:22:39 2006 +0100 @@ -13,7 +13,7 @@ instance set :: (eq) eq .. -lemma [code target: Set, code nofunc]: +lemma [code target: Set]: "(A = B) = (A \<subseteq> B \<and> B \<subseteq> A)" by blast