tuned comment
authorhaftmann
Sat Jun 11 07:50:28 2011 +0200 (2011-06-11)
changeset 43363eaf8b7f22d39
parent 43362 8d3a5b7b9a00
child 43364 9c392ea6a6e6
tuned comment
src/HOL/Library/Executable_Set.thy
     1.1 --- a/src/HOL/Library/Executable_Set.thy	Fri Jun 10 17:52:09 2011 +0200
     1.2 +++ b/src/HOL/Library/Executable_Set.thy	Sat Jun 11 07:50:28 2011 +0200
     1.3 @@ -12,7 +12,7 @@
     1.4  text {*
     1.5    This is just an ad-hoc hack which will rarely give you what you want.
     1.6    For the moment, whenever you need executable sets, consider using
     1.7 -  type @{text fset} from theory @{text Cset}.
     1.8 +  type @{text Cset.set} from theory @{text Cset}.
     1.9  *}
    1.10  
    1.11  declare mem_def [code del]