doc-src/IsarRef/Thy/HOL_Specific.thy
changeset 40711 81bc73585eec
parent 40709 b29c70cd5c93
child 40800 330eb65c9469
     1.1 --- a/doc-src/IsarRef/Thy/HOL_Specific.thy	Fri Nov 26 12:03:17 2010 +0100
     1.2 +++ b/doc-src/IsarRef/Thy/HOL_Specific.thy	Fri Nov 26 12:03:18 2010 +0100
     1.3 @@ -1082,7 +1082,7 @@
     1.4      const: term
     1.5      ;
     1.6  
     1.7 -    constexpr: ( const | 'name.*' | '*' )
     1.8 +    constexpr: ( const | 'name._' | '_' )
     1.9      ;
    1.10  
    1.11      typeconstructor: nameref
    1.12 @@ -1144,7 +1144,7 @@
    1.13      ;
    1.14  
    1.15      'code_reflect' string \\
    1.16 -      ( 'datatypes' ( string '=' ( '"*"' | ( string + '|' ) + 'and' ) ) ) ? \\
    1.17 +      ( 'datatypes' ( string '=' ( '_' | ( string + '|' ) + 'and' ) ) ) ? \\
    1.18        ( 'functions' ( string + ) ) ? ( 'file' string ) ?
    1.19      ;
    1.20