src/HOL/Library/RBT_Set.thy
changeset 49948 744934b818c7
parent 49928 e3f0a92de280
child 50996 51ad7b4ac096
     1.1 --- a/src/HOL/Library/RBT_Set.thy	Sat Oct 20 09:09:37 2012 +0200
     1.2 +++ b/src/HOL/Library/RBT_Set.thy	Sat Oct 20 09:12:16 2012 +0200
     1.3 @@ -63,6 +63,11 @@
     1.4  lemma [code, code del]:
     1.5    "Bex = Bex" ..
     1.6  
     1.7 +term can_select
     1.8 +
     1.9 +lemma [code, code del]:
    1.10 +  "can_select = can_select" ..
    1.11 +
    1.12  lemma [code, code del]:
    1.13    "Set.union = Set.union" ..
    1.14