# HG changeset patch
# User tbourke
# Date 1256250022 -39600
# Node ID e6eda76ad49e4d84cb990d5d08848c65221e4b3b
# Parent  2f6ce3b9ec394029b45c4e6c43be644cd8b4c575
Fix a duplicate abbreviation || in etc/symbols.

diff -r 2f6ce3b9ec39 -r e6eda76ad49e etc/symbols
--- a/etc/symbols	Thu Oct 22 17:54:47 2009 +0200
+++ b/etc/symbols	Fri Oct 23 09:20:22 2009 +1100
@@ -244,7 +244,7 @@
 \<Inter>                code: 0x0022c2  font: Isabelle  abbrev: Inter
 \<union>                code: 0x00222a  font: Isabelle  abbrev: Un
 \<Union>                code: 0x0022c3  font: Isabelle  abbrev: Union
-\<squnion>              code: 0x002294  font: Isabelle  abbrev: ||
+\<squnion>              code: 0x002294  font: Isabelle  abbrev: |_|
 \<Squnion>              code: 0x002a06  font: Isabelle  abbrev: |||
 \<sqinter>              code: 0x002293  font: Isabelle  abbrev: &&
 \<Sqinter>              code: 0x002a05  font: Isabelle  abbrev: &&&