src/HOL/Library/RBT_Set.thy
changeset 57816 d8bbb97689d3
parent 57514 bdc2c6b40bf2
child 58301 de95aeedf49e
     1.1 --- a/src/HOL/Library/RBT_Set.thy	Thu Aug 07 12:17:41 2014 +0200
     1.2 +++ b/src/HOL/Library/RBT_Set.thy	Thu Aug 07 12:17:41 2014 +0200
     1.3 @@ -522,7 +522,7 @@
     1.4  
     1.5  code_datatype Set Coset
     1.6  
     1.7 -declare set_simps[code]
     1.8 +declare list.set[code] (* needed? *)
     1.9  
    1.10  lemma empty_Set [code]:
    1.11    "Set.empty = Set RBT.empty"