# HG changeset patch
# User wenzelm
# Date 859886166 -7200
# Node ID a66196e1668c7fdd3cab046c4a2bb963c6ec74fc
# Parent  01a536a6e4fb575b54e30fd54405a205d71edfb3
removed useless symbol font syntax;

diff -r 01a536a6e4fb -r a66196e1668c src/HOLCF/Porder0.thy
--- a/src/HOLCF/Porder0.thy	Tue Apr 01 09:28:56 1997 +0200
+++ b/src/HOLCF/Porder0.thy	Tue Apr 01 11:16:06 1997 +0200
@@ -11,7 +11,7 @@
 
 (* first the global constant for HOLCF type classes *)
 consts
-  "less"        :: "['a,'a] => bool" (infixl "\\<sqsubseteq>\\<sqsubseteq>" 55)
+  "less"        :: "['a,'a] => bool"
 
 axclass po < term
         (* class axioms: *)