--- a/doc-src/IsarRef/Thy/document/HOL_Specific.tex Fri Nov 26 12:03:17 2010 +0100
+++ b/doc-src/IsarRef/Thy/document/HOL_Specific.tex Fri Nov 26 12:03:18 2010 +0100
@@ -1098,7 +1098,7 @@
const: term
;
- constexpr: ( const | 'name.*' | '*' )
+ constexpr: ( const | 'name._' | '_' )
;
typeconstructor: nameref
@@ -1160,7 +1160,7 @@
;
'code_reflect' string \\
- ( 'datatypes' ( string '=' ( '"*"' | ( string + '|' ) + 'and' ) ) ) ? \\
+ ( 'datatypes' ( string '=' ( '_' | ( string + '|' ) + 'and' ) ) ) ? \\
( 'functions' ( string + ) ) ? ( 'file' string ) ?
;