author | haftmann |
Fri, 03 Nov 2006 14:22:39 +0100 | |
changeset 21153 | 8288c8f203de |
parent 21152 | e97992896170 |
child 21154 | c8cc6b68759f |
--- 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