src/HOL/Import/Generate-HOLLight/GenHOLLight.thy

--- a/src/HOL/Import/Generate-HOLLight/GenHOLLight.thy	Sat Sep 17 01:50:01 2005 +0200
+++ b/src/HOL/Import/Generate-HOLLight/GenHOLLight.thy	Sat Sep 17 11:49:29 2005 +0200
@@ -41,6 +41,10 @@
   num > nat;
  (* sum > "+";*)
 
+const_renames
+  "==" > "eqeq"
+  ".." > "dotdot";
+
 const_maps
   T > True
   F > False