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.
'notation': more robust 'and' list;
authorwenzelm
Fri, 17 Nov 2006 02:19:55 +0100
changeset 21403 dd58f13a8eb4
parent 21402 c15bcd87f47c
child 21404 eb85850d3eb7
'notation': more robust 'and' list;
doc-src/IsarRef/generic.tex file | annotate | diff | comparison | revisions
src/Pure/Isar/isar_syn.ML file | annotate | diff | comparison | revisions 
--- a/doc-src/IsarRef/generic.tex	Fri Nov 17 02:19:54 2006 +0100
+++ b/doc-src/IsarRef/generic.tex	Fri Nov 17 02:19:55 2006 +0100
@@ -29,7 +29,7 @@
   ;
   'abbreviation' target? mode? (constdecl? prop +)
   ;
-  'notation' target? mode? (nameref mixfix +)
+  'notation' target? mode? (nameref mixfix + 'and')
   ;
 
   consts: ((name ('::' type)? structmixfix? | vars) + 'and')
--- a/src/Pure/Isar/isar_syn.ML	Fri Nov 17 02:19:54 2006 +0100
+++ b/src/Pure/Isar/isar_syn.ML	Fri Nov 17 02:19:55 2006 +0100
@@ -218,7 +218,7 @@
 
 val notationP =
   OuterSyntax.command "notation" "variable/constant syntax" K.thy_decl
-    (P.opt_locale_target -- opt_mode -- Scan.repeat1 (P.xname -- P.mixfix)
+    (P.opt_locale_target -- opt_mode -- P.and_list1 (P.xname -- P.mixfix)
     >> (fn ((loc, mode), args) =>
         Toplevel.local_theory loc (Specification.notation mode args)));
isabelle