changeset 52435 | 6646bb548c6b |
parent 52378 | 08dbf9ff2140 |
child 52476 | 7d7b4e285ea7 |
--- a/src/Doc/IsarRef/HOL_Specific.thy Sun Jun 23 21:16:06 2013 +0200 +++ b/src/Doc/IsarRef/HOL_Specific.thy Sun Jun 23 21:16:07 2013 +0200 @@ -2224,7 +2224,7 @@ @{rail " @@{command (HOL) export_code} ( constexpr + ) \\ ( ( @'in' target ( @'module_name' @{syntax string} ) ? \\ - ( @'file' ( @{syntax string} | '-' ) ) ? ( '(' args ')' ) ?) + ) ? + ( @'file' @{syntax string} ) ? ( '(' args ')' ) ?) + ) ? ; const: @{syntax term}