removed slightly exotic symbol abbreviations for now -- achieves a coherent (unique) mapping;
authorwenzelm
Thu, 29 Oct 2009 11:26:47 +0100
changeset 33300 939ca97f5a11
parent 33299 73af7831ba1e
child 33301 1fe9fc908ec3
child 33322 6ff4674499ca
child 33566 1c62ac4ef6d1
removed slightly exotic symbol abbreviations for now -- achieves a coherent (unique) mapping; (NB: in principle symbol abbreviations could well be ambigous);
etc/symbols
--- a/etc/symbols	Thu Oct 29 10:52:05 2009 +0100
+++ b/etc/symbols	Thu Oct 29 11:26:47 2009 +0100
@@ -244,10 +244,10 @@
 \<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: 0x002a06  font: Isabelle  abbrev: |||
-\<sqinter>              code: 0x002293  font: Isabelle  abbrev: &&
-\<Sqinter>              code: 0x002a05  font: Isabelle  abbrev: &&&
+\<squnion>              code: 0x002294  font: Isabelle
+\<Squnion>              code: 0x002a06  font: Isabelle
+\<sqinter>              code: 0x002293  font: Isabelle
+\<Sqinter>              code: 0x002a05  font: Isabelle
 \<setminus>             code: 0x002216  font: Isabelle
 \<propto>               code: 0x00221d  font: Isabelle
 \<uplus>                code: 0x00228e  font: Isabelle