diff options
| author | Makarius Wenzel | 2001-12-01 18:04:47 +0000 |
|---|---|---|
| committer | Makarius Wenzel | 2001-12-01 18:04:47 +0000 |
| commit | 4b77e6ad1f926665da6b27af3ed52dd768469c80 (patch) | |
| tree | d9460e99e9d14a7268c5090710521a8f9063b242 /html/functions.php3 | |
| parent | 9cc1a6455b44774d43e103d27863991560483df6 (diff) | |
\<euro> symbol;
use previously defined x-symbol-isabelle-user-table (or nil);
x-symbol-user-table achieves electric |- and |= symbols;
Diffstat (limited to 'html/functions.php3')
0 files changed, 0 insertions, 0 deletions