changeset 40709 | b29c70cd5c93 |
parent 40388 | cb9fd7dd641c |
child 40711 | 81bc73585eec |
--- a/doc-src/IsarRef/Thy/HOL_Specific.thy Fri Nov 26 11:06:49 2010 +0100 +++ b/doc-src/IsarRef/Thy/HOL_Specific.thy Fri Nov 26 11:38:20 2010 +0100 @@ -1143,7 +1143,8 @@ 'code_modulename' target ( ( string string ) + ) ; - 'code_reflect' string ( 'datatypes' ( string '=' ( string + '|' ) + 'and' ) ) ? \\ + 'code_reflect' string \\ + ( 'datatypes' ( string '=' ( '"*"' | ( string + '|' ) + 'and' ) ) ) ? \\ ( 'functions' ( string + ) ) ? ( 'file' string ) ? ;