Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
datatype constructor glob for code_reflect
authorhaftmann
Fri, 26 Nov 2010 11:38:20 +0100
changeset 40709 b29c70cd5c93
parent 40708 739dc2c2ba24
child 40710 499aa989fbad
datatype constructor glob for code_reflect
doc-src/IsarRef/Thy/HOL_Specific.thy file | annotate | diff | comparison | revisions
doc-src/IsarRef/Thy/document/HOL_Specific.tex file | annotate | diff | comparison | revisions 
--- 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 ) ?
     ;
 
--- a/doc-src/IsarRef/Thy/document/HOL_Specific.tex	Fri Nov 26 11:06:49 2010 +0100
+++ b/doc-src/IsarRef/Thy/document/HOL_Specific.tex	Fri Nov 26 11:38:20 2010 +0100
@@ -1159,7 +1159,8 @@
     'code_modulename' target ( ( string string ) + )
     ;
 
-    'code_reflect' string ( 'datatypes' ( string '=' ( string + '|' ) + 'and' ) ) ? \\
+    'code_reflect' string \\
+      ( 'datatypes' ( string '=' ( '"*"' | ( string + '|' ) + 'and' ) ) ) ? \\
       ( 'functions' ( string + ) ) ? ( 'file' string ) ?
     ;
isabelle