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.
Oracles can now be strings instead of identifiers
authorpaulson
Thu, 11 Jul 1996 15:18:57 +0200
changeset 1850 c6b6ccfd390c
parent 1849 bec272e3e888
child 1851 7b1e1c298e50
Oracles can now be strings instead of identifiers
src/Pure/Thy/thy_parse.ML file | annotate | diff | comparison | revisions 
--- a/src/Pure/Thy/thy_parse.ML	Thu Jul 11 15:14:41 1996 +0200
+++ b/src/Pure/Thy/thy_parse.ML	Thu Jul 11 15:18:57 1996 +0200
@@ -523,7 +523,7 @@
   "{", "}", "(", ")", "[", "]", "::", "==", "=>", "<="];
 
 val pure_sections =
- [section "oracle" "|> set_oracle" ident,
+ [section "oracle" "|> set_oracle" (name >> strip_quotes),
   section "classes" "|> add_classes" class_decls,
   section "default" "|> add_defsort" sort,
   section "types" "" type_decls,
isabelle