# HG changeset patch # User wenzelm # Date 794142440 -3600 # Node ID 6bee3815c0bfe5d199a0b12e9ba312f2f8faceba # Parent b162fe4ae444d22c21b8fe1ec43148298c47dd7a added declaration of syntactic const "_abs"; diff -r b162fe4ae444 -r 6bee3815c0bf src/Pure/Syntax/mixfix.ML --- a/src/Pure/Syntax/mixfix.ML Tue Feb 28 10:54:49 1995 +0100 +++ b/src/Pure/Syntax/mixfix.ML Thu Mar 02 12:07:20 1995 +0100 @@ -144,6 +144,7 @@ val pure_syntax = [("_lambda", "[idts, 'a] => logic", Mixfix ("(3%_./ _)", [], 0)), + ("_abs", "'a", NoSyn), ("", "'a => " ^ args, Delimfix "_"), ("_args", "['a, " ^ args ^ "] => " ^ args, Delimfix "_,/ _"), ("", "id => idt", Delimfix "_"),