changeset 54338 | 7518a89965fe |
parent 54334 | 409d7f7247f4 |
child 54890 | cb892d835803 |
--- a/src/Doc/IsarRef/HOL_Specific.thy Mon Oct 14 15:13:11 2013 +0200 +++ b/src/Doc/IsarRef/HOL_Specific.thy Mon Oct 14 15:46:35 2013 +0200 @@ -2529,7 +2529,7 @@ ; @@{command (HOL) code_include} target ( @{syntax string} ( @{syntax string} | '-') ) - ;cite + ; @@{command (HOL) code_identifier} ( ( symbol_const | symbol_typeconstructor | symbol_class | symbol_class_relation | symbol_class_instance