author | Andreas Lochbihler |
Tue, 26 Jul 2011 14:05:28 +0200 | |
changeset 44850 | 9f27d2bf4087 |
parent 44848 | 0eb2b12bd99e |
child 44851 | 995c2534c3fe |
1.1 --- a/src/HOL/Library/List_Cset.thy Tue Jul 26 12:44:36 2011 +0200 1.2 +++ b/src/HOL/Library/List_Cset.thy Tue Jul 26 14:05:28 2011 +0200 1.3 @@ -133,7 +133,7 @@ 1.4 1.5 end 1.6 1.7 -declare single_code [code del] 1.8 +declare Cset.single_code [code del] 1.9 lemma single_set [code]: 1.10 "Cset.single a = Cset.set [a]" 1.11 by(simp add: Cset.single_code)