# HG changeset patch
# User wenzelm
# Date 972491620 -7200
# Node ID e5e6070fcef55a66461b5600e4c746aeb1664815
# Parent  f12ff6a4bc7bea6fada90d5029bf1d956c09ee27
add \<le> to list of "good" symbols;

diff -r f12ff6a4bc7b -r e5e6070fcef5 src/HOL/Library/README.html
--- a/src/HOL/Library/README.html	Wed Oct 25 18:33:01 2000 +0200
+++ b/src/HOL/Library/README.html	Wed Oct 25 18:33:40 2000 +0200
@@ -91,6 +91,7 @@
 <tt>\&lt;and&gt;</tt>,
 <tt>\&lt;in&gt;</tt>,
 <tt>\&lt;inter&gt;</tt>,
+<tt>\&lt;le&gt;</tt>,
 <tt>\&lt;not&gt;</tt>,
 <tt>\&lt;noteq&gt;</tt>,
 <tt>\&lt;notin&gt;</tt>,