@noindent
In the documentation below, such cases are simply marked
-as being equivalent to the corresponding pragma or attribute definition
-clause.
+as being boolean aspects equivalent to the corresponding pragma
+or attribute definition clause.
@menu
* Aspect Abstract_State::
@unnumberedsec Aspect Async_Readers
@findex Async_Readers
@noindent
-This aspect is equivalent to pragma @code{Async_Readers}.
+This boolean aspect is equivalent to pragma @code{Async_Readers}.
@node Aspect Async_Writers
@unnumberedsec Aspect Async_Writers
@findex Async_Writers
@noindent
-This aspect is equivalent to pragma @code{Async_Writers}.
+This boolean aspect is equivalent to pragma @code{Async_Writers}.
@node Aspect Contract_Cases
@unnumberedsec Aspect Contract_Cases
@unnumberedsec Aspect Favor_Top_Level
@findex Favor_Top_Level
@noindent
-This aspect is equivalent to pragma @code{Favor_Top_Level}.
+This boolean aspect is equivalent to pragma @code{Favor_Top_Level}.
@node Aspect Global
@unnumberedsec Aspect Global
@unnumberedsec Aspect Inline_Always
@findex Inline_Always
@noindent
-This aspect is equivalent to pragma @code{Inline_Always}.
+This boolean aspect is equivalent to pragma @code{Inline_Always}.
@node Aspect Invariant
@unnumberedsec Aspect Invariant
@unnumberedsec Aspect Lock_Free
@findex Lock_Free
@noindent
-This aspect is equivalent to pragma @code{Lock_Free}.
+This boolean aspect is equivalent to pragma @code{Lock_Free}.
@node Aspect No_Elaboration_Code_All
@unnumberedsec Aspect No_Elaboration_Code_All
@unnumberedsec Aspect Persistent_BSS
@findex Persistent_BSS
@noindent
-This aspect is equivalent to pragma @code{Persistent_BSS}.
+This boolean aspect is equivalent to pragma @code{Persistent_BSS}.
@node Aspect Predicate
@unnumberedsec Aspect Predicate
@unnumberedsec Aspect Pure_Function
@findex Pure_Function
@noindent
-This aspect is equivalent to pragma @code{Pure_Function}.
+This boolean aspect is equivalent to pragma @code{Pure_Function}.
@node Aspect Refined_Depends
@unnumberedsec Aspect Refined_Depends
@unnumberedsec Aspect Shared
@findex Shared
@noindent
-This aspect is equivalent to pragma @code{Shared}, and is thus a synonym
-for aspect @code{Atomic}.
+This booleanaspect is equivalent to pragma @code{Shared},
+and is thus a synonym for aspect @code{Atomic}.
@node Aspect Simple_Storage_Pool
@unnumberedsec Aspect Simple_Storage_Pool
@unnumberedsec Aspect Simple_Storage_Pool_Type
@findex Simple_Storage_Pool_Type
@noindent
-This aspect is equivalent to pragma @code{Simple_Storage_Pool_Type}.
+This boolean aspect is equivalent to pragma @code{Simple_Storage_Pool_Type}.
@node Aspect SPARK_Mode
@unnumberedsec Aspect SPARK_Mode
@unnumberedsec Aspect Suppress_Debug_Info
@findex Suppress_Debug_Info
@noindent
-This aspect is equivalent to pragma @code{Suppress_Debug_Info}.
+This boolean aspect is equivalent to pragma @code{Suppress_Debug_Info}.
@node Aspect Test_Case
@unnumberedsec Aspect Test_Case
@unnumberedsec Aspect Thread_Local_Storage
@findex Thread_Local_Storage
@noindent
-This aspect is equivalent to pragma @code{Thread_Local_Storage}.
+This boolean aspect is equivalent to pragma @code{Thread_Local_Storage}.
@node Aspect Universal_Aliasing
@unnumberedsec Aspect Universal_Aliasing
@findex Universal_Aliasing
@noindent
-This aspect is equivalent to pragma @code{Universal_Aliasing}.
+This boolean aspect is equivalent to pragma @code{Universal_Aliasing}.
@node Aspect Universal_Data
@unnumberedsec Aspect Universal_Data
@unnumberedsec Aspect Unmodified
@findex Unmodified
@noindent
-This aspect is equivalent to pragma @code{Unmodified}.
+This boolean aspect is equivalent to pragma @code{Unmodified}.
@node Aspect Unreferenced
@unnumberedsec Aspect Unreferenced
@findex Unreferenced
@noindent
-This aspect is equivalent to pragma @code{Unreferenced}.
+This boolean aspect is equivalent to pragma @code{Unreferenced}. Note that
+in the case of formal parameters, it is not permitted to have aspects for
+a formal parameter, so in this case the pragma form must be used.
@node Aspect Unreferenced_Objects
@unnumberedsec Aspect Unreferenced_Objects
@findex Unreferenced_Objects
@noindent
-This aspect is equivalent to pragma @code{Unreferenced_Objects}.
+This boolean aspect is equivalent to pragma @code{Unreferenced_Objects}.
@node Aspect Value_Size
@unnumberedsec Aspect Value_Size