--- a/src/Pure/Isar/args.ML Wed Sep 13 22:29:37 2000 +0200
+++ b/src/Pure/Isar/args.ML Wed Sep 13 22:31:19 2000 +0200
@@ -29,6 +29,8 @@
val nat: T list -> int * T list
val int: T list -> int * T list
val var: T list -> indexname * T list
+ val addN: string
+ val delN: string
val enum: string -> ('a * T list -> 'b * ('a * T list)) -> 'a * T list -> 'b list * ('a * T list)
val enum1: string -> ('a * T list -> 'b * ('a * T list)) -> 'a * T list -> 'b list * ('a * T list)
val and_list: ('a * T list -> 'b * ('a * T list)) -> 'a * T list -> 'b list * ('a * T list)
@@ -135,6 +137,9 @@
val int = Scan.optional ($$$ "-" >> K ~1) 1 -- nat >> op *;
val var = kind (apsome #1 o try Term.dest_Var o Syntax.read_var);
+val addN = "add";
+val delN = "del";
+
(* enumerations *)