# HG changeset patch
# User wenzelm
# Date 962031235 -7200
# Node ID b7642408aea3f102331d51956d2dfb5b6df52543
# Parent  a126a40cba76833e4bbabb878eafc9da537e1c77
avoid \< in input;

diff -r a126a40cba76 -r b7642408aea3 src/HOL/UNITY/AllocImpl.ML
--- a/src/HOL/UNITY/AllocImpl.ML	Mon Jun 26 16:53:37 2000 +0200
+++ b/src/HOL/UNITY/AllocImpl.ML	Mon Jun 26 16:53:55 2000 +0200
@@ -134,7 +134,7 @@
 \ (INT i : lessThan Nclients.   \
 \  INT h. {s. h <= (sub i o allocGiv)s & h pfixGe (sub i o allocAsk)s}  \
 \          LeadsTo {s. tokens h <= (tokens o sub i o allocRel)s})        \
-\<=     \
+\ <=     \
 \(INT i : lessThan Nclients. Increasing (sub i o allocAsk) Int  \
 \                            Increasing (sub i o allocRel))     \
 \ Int   \