'notation': more robust 'and' list;
authorwenzelm
Fri Nov 17 02:19:55 2006 +0100 (2006-11-17 ago)
changeset 21403dd58f13a8eb4
parent 21402 c15bcd87f47c
child 21404 eb85850d3eb7
'notation': more robust 'and' list;
doc-src/IsarRef/generic.tex
src/Pure/Isar/isar_syn.ML
     1.1 --- a/doc-src/IsarRef/generic.tex	Fri Nov 17 02:19:54 2006 +0100
     1.2 +++ b/doc-src/IsarRef/generic.tex	Fri Nov 17 02:19:55 2006 +0100
     1.3 @@ -29,7 +29,7 @@
     1.4    ;
     1.5    'abbreviation' target? mode? (constdecl? prop +)
     1.6    ;
     1.7 -  'notation' target? mode? (nameref mixfix +)
     1.8 +  'notation' target? mode? (nameref mixfix + 'and')
     1.9    ;
    1.10  
    1.11    consts: ((name ('::' type)? structmixfix? | vars) + 'and')
     2.1 --- a/src/Pure/Isar/isar_syn.ML	Fri Nov 17 02:19:54 2006 +0100
     2.2 +++ b/src/Pure/Isar/isar_syn.ML	Fri Nov 17 02:19:55 2006 +0100
     2.3 @@ -218,7 +218,7 @@
     2.4  
     2.5  val notationP =
     2.6    OuterSyntax.command "notation" "variable/constant syntax" K.thy_decl
     2.7 -    (P.opt_locale_target -- opt_mode -- Scan.repeat1 (P.xname -- P.mixfix)
     2.8 +    (P.opt_locale_target -- opt_mode -- P.and_list1 (P.xname -- P.mixfix)
     2.9      >> (fn ((loc, mode), args) =>
    2.10          Toplevel.local_theory loc (Specification.notation mode args)));
    2.11