# HG changeset patch # User wenzelm # Date 1245783618 -7200 # Node ID 68eccca7f51ca0793c79667e5e5f4b5321359a3c # Parent eb174cfdef1a4e91162247a9ea7d96443ccaf5f2 fixed abbrev !! for \; diff -r eb174cfdef1a -r 68eccca7f51c etc/symbols --- a/etc/symbols Tue Jun 23 20:14:40 2009 +0200 +++ b/etc/symbols Tue Jun 23 21:00:18 2009 +0200 @@ -207,7 +207,7 @@ \ code: 0x0022a5 font: Isabelle \ code: 0x0022a4 font: Isabelle \ code: 0x002227 font: Isabelle abbrev: /\ -\ code: 0x0022c0 font: Isabelle abbreb: !! +\ code: 0x0022c0 font: Isabelle abbrev: !! \ code: 0x002228 font: Isabelle abbrev: \/ \ code: 0x0022c1 font: Isabelle abbrev: ?? \ code: 0x002200 font: Isabelle abbrev: !