datatype constructor glob for code_reflect
authorhaftmann
Fri Nov 26 11:38:20 2010 +0100 (2010-11-26)
changeset 40709b29c70cd5c93
parent 40708 739dc2c2ba24
child 40710 499aa989fbad
datatype constructor glob for code_reflect
doc-src/IsarRef/Thy/HOL_Specific.thy
doc-src/IsarRef/Thy/document/HOL_Specific.tex
     1.1 --- a/doc-src/IsarRef/Thy/HOL_Specific.thy	Fri Nov 26 11:06:49 2010 +0100
     1.2 +++ b/doc-src/IsarRef/Thy/HOL_Specific.thy	Fri Nov 26 11:38:20 2010 +0100
     1.3 @@ -1143,7 +1143,8 @@
     1.4      'code_modulename' target ( ( string string ) + )
     1.5      ;
     1.6  
     1.7 -    'code_reflect' string ( 'datatypes' ( string '=' ( string + '|' ) + 'and' ) ) ? \\
     1.8 +    'code_reflect' string \\
     1.9 +      ( 'datatypes' ( string '=' ( '"*"' | ( string + '|' ) + 'and' ) ) ) ? \\
    1.10        ( 'functions' ( string + ) ) ? ( 'file' string ) ?
    1.11      ;
    1.12  
     2.1 --- a/doc-src/IsarRef/Thy/document/HOL_Specific.tex	Fri Nov 26 11:06:49 2010 +0100
     2.2 +++ b/doc-src/IsarRef/Thy/document/HOL_Specific.tex	Fri Nov 26 11:38:20 2010 +0100
     2.3 @@ -1159,7 +1159,8 @@
     2.4      'code_modulename' target ( ( string string ) + )
     2.5      ;
     2.6  
     2.7 -    'code_reflect' string ( 'datatypes' ( string '=' ( string + '|' ) + 'and' ) ) ? \\
     2.8 +    'code_reflect' string \\
     2.9 +      ( 'datatypes' ( string '=' ( '"*"' | ( string + '|' ) + 'and' ) ) ) ? \\
    2.10        ( 'functions' ( string + ) ) ? ( 'file' string ) ?
    2.11      ;
    2.12