# HG changeset patch # User wenzelm # Date 1530004247 -7200 # Node ID 8d9239158d7a294de3e3b895680aa02b8b01c9e9 # Parent f483fe1813f0c5959eb6311af8dd39f1c6af9ed7 tuned; diff -r f483fe1813f0 -r 8d9239158d7a src/Doc/Isar_Ref/Inner_Syntax.thy --- a/src/Doc/Isar_Ref/Inner_Syntax.thy Tue Jun 26 10:49:37 2018 +0200 +++ b/src/Doc/Isar_Ref/Inner_Syntax.thy Tue Jun 26 11:10:47 2018 +0200 @@ -391,7 +391,7 @@ atom: @{syntax short_ident} | @{syntax int} | @{syntax float} | @{syntax cartouche} \} - Each @{syntax entry} is a name-value pair: if the value is omitted, if + Each @{syntax entry} is a name-value pair: if the value is omitted, it defaults to \<^verbatim>\true\ (intended for Boolean properties). The following standard block properties are supported: