added int;
authorwenzelm
Fri Aug 04 23:00:15 2000 +0200 (2000-08-04)
changeset 95383af720af9cd9
parent 9537 7e0ba737f98e
child 9539 7ff8f3516d54
added int;
src/Pure/Isar/args.ML
     1.1 --- a/src/Pure/Isar/args.ML	Fri Aug 04 23:00:01 2000 +0200
     1.2 +++ b/src/Pure/Isar/args.ML	Fri Aug 04 23:00:15 2000 +0200
     1.3 @@ -25,6 +25,7 @@
     1.4    val name: T list -> string * T list
     1.5    val name_dummy: T list -> string option * T list
     1.6    val nat: T list -> int * T list
     1.7 +  val int: T list -> int * T list
     1.8    val var: T list -> indexname * T list
     1.9    val enum: string -> ('a * T list -> 'b * ('a * T list)) -> 'a * T list -> 'b list * ('a * T list)
    1.10    val enum1: string -> ('a * T list -> 'b * ('a * T list)) -> 'a * T list -> 'b list * ('a * T list)
    1.11 @@ -123,6 +124,7 @@
    1.12    | _ => Scan.fail) >> #2;
    1.13  
    1.14  val nat = kind Syntax.read_nat;
    1.15 +val int = Scan.optional ($$$ "-" >> K ~1) 1 -- nat >> op *;
    1.16  val var = kind (apsome #1 o try Term.dest_Var o Syntax.read_var);
    1.17  
    1.18