src/HOL/Library/RBT_Set.thy
changeset 58301 de95aeedf49e
parent 57816 d8bbb97689d3
child 58368 fe083c681ed8
     1.1 --- a/src/HOL/Library/RBT_Set.thy	Thu Sep 11 18:54:36 2014 +0200
     1.2 +++ b/src/HOL/Library/RBT_Set.thy	Thu Sep 11 18:54:36 2014 +0200
     1.3 @@ -10,7 +10,7 @@
     1.4  
     1.5  (*
     1.6    Users should be aware that by including this file all code equations
     1.7 -  outside of List.thy using 'a list as an implenentation of sets cannot be
     1.8 +  outside of List.thy using 'a list as an implementation of sets cannot be
     1.9    used for code generation. If such equations are not needed, they can be
    1.10    deleted from the code generator. Otherwise, a user has to provide their 
    1.11    own equations using RBT trees.