changeset 37379 | f23e60581eb3 |
parent 36453 | 2f383885d8f8 |
child 37422 | 6d19e4e6ebf5 |
--- a/doc-src/IsarRef/Thy/document/HOL_Specific.tex Thu Jun 10 12:08:33 2010 +0200 +++ b/doc-src/IsarRef/Thy/document/HOL_Specific.tex Mon Jun 14 10:38:28 2010 +0200 @@ -1082,7 +1082,7 @@ target: 'OCaml' | 'SML' | 'Haskell' ; - 'code\_datatype' const + + 'code\_datatype' ( const + ) ; 'code\_const' (const + 'and') \\