History log of /seL4-l4v-master/isabelle/etc/symbols
Revision Date Author Comments
# f760949e 17-Aug-2019 wenzelm <none@none>

added ML antiquotation @{oracle_name};


# 68d70025 17-Jul-2019 wenzelm <none@none>

added \<llangle>, \<rrangle>;
discontinued special rendering for old {* *};


# 468cf5fb 17-Jul-2019 wenzelm <none@none>

added \<bbar>;


# baa5a8c5 17-Jul-2019 wenzelm <none@none>

added \<sqdot>;


# e1f0becb 28-Apr-2019 wenzelm <none@none>

completion for \<^const>, although it often requires an extra argument;


# 886a0067 30-Mar-2019 wenzelm <none@none>

clarified signature: more explicit type Path.binding;
tuned;


# d8c6845a 10-Mar-2019 wenzelm <none@none>

document markers are formal comments, and may thus occur anywhere in the command-span;
clarified Outer_Syntax.parse_span, Outer_Syntax.parse_text wrt. span structure;
tuned signature;


# 645710b2 09-Mar-2019 wenzelm <none@none>

added glyph for \<marker>;


# a095d5ee 28-Nov-2018 wenzelm <none@none>

clarified symbol groups;


# 7023c8c4 24-Nov-2018 wenzelm <none@none>

use "Isabelle DejaVu" fonts uniformly: Text Area, GUI elements, HTML output etc.;


# cab4a832 19-Jan-2018 wenzelm <none@none>

support for completion;


# 98bd15fa 14-Jan-2018 wenzelm <none@none>

support for completion;


# 2bf3a1cf 13-Jan-2018 wenzelm <none@none>

added glyph from "Deja Vu Sans Mono" font;


# dc534bc8 13-Jan-2018 wenzelm <none@none>

added \<^cancel> operator for unused text;


# 22f29a40 01-Jan-2018 wenzelm <none@none>

more completion templates;


# 12060e54 30-Dec-2017 wenzelm <none@none>

more robust hyphen (see also "Soft hyphen (SHY) – a hard problem?" http://jkorpela.fi/shy.html);


# 401e509b 13-Dec-2016 wenzelm <none@none>

more symbols;


# aa265bd5 30-Aug-2016 wenzelm <none@none>

added glyph from "Deja Vu Sans Mono" font;


# 360dd89e 12-Aug-2016 wenzelm <none@none>

some icons from Symbola font;


# ef474b78 27-Feb-2016 wenzelm <none@none>

symbol interpretation for \<circle>;


# 8341fc80 04-Feb-2016 wenzelm <none@none>

clarified;


# b353ffd6 23-Jan-2016 wenzelm <none@none>

discontinued irregular abbrevs: ".o" counts as word, "+o", "*o", "-o" are occasionally used as ASCII notation, "*o" is in conflict with "(*o" in comments;


# 0dfec37b 08-Jan-2016 wenzelm <none@none>

\<struct> loses its rendering and is superseded by \<diamondop>;
tuned;


# 7033ce1b 01-Jan-2016 wenzelm <none@none>

clarified abbrev;


# e1f6237b 01-Jan-2016 wenzelm <none@none>

clarified groups, notably for Symbols dockable;


# 99c05d59 01-Jan-2016 wenzelm <none@none>

glyphs for \<bind>, \<then>;


# d137f020 29-Dec-2015 wenzelm <none@none>

simplified abbrevs: exploit ambiguity;


# d4149472 29-Dec-2015 wenzelm <none@none>

more arrow symbols;


# f8cc5c15 29-Dec-2015 wenzelm <none@none>

more arrow symbols;


# fc743940 12-Nov-2015 wenzelm <none@none>

support short form for \<^theory_text>;


# 72638be3 06-Nov-2015 wenzelm <none@none>

added @{undefined} with somewhat undefined symbol;


# 380b6e10 06-Nov-2015 wenzelm <none@none>

retain traditional rendering of \<paragraph>;


# b2bc23d4 05-Nov-2015 wenzelm <none@none>

IsabelleText for unusual symbol;


# a2ea8657 04-Nov-2015 wenzelm <none@none>

symbolic syntax "\<comment> text";


# 5d43b0e7 04-Nov-2015 wenzelm <none@none>

document antiquotation @{footnote};
render \<^footnote> as pilcrow -- the rarely used \<paragraph> loses its interpretation;


# 0dd7cab7 21-Oct-2015 wenzelm <none@none>

rendering for \<^verbatim>;


# e7d896ea 18-Oct-2015 wenzelm <none@none>

clarified control antiquotations: decode control symbol to get name;
document antiquotations @{emph}, @{bold};
symbol interpretation for \<^emph>;
tuned;


# c613ba35 15-Oct-2015 wenzelm <none@none>

unused -- avoid confusion in Symbols dockable;


# 674cbaa9 14-Oct-2015 wenzelm <none@none>

clarified control symbols;


# e8364dc3 12-Oct-2015 wenzelm <none@none>

some control symbols for markup and formatting;


# 9f747857 08-Apr-2015 wenzelm <none@none>

added symbol for \<hole> (from DejaVuSansMono and DejaVuSansMono-Bold version 2.34);


# f5cbdf73 23-May-2014 wenzelm <none@none>

receovered alternative abbrevs for \<open> \<close> from 8e8243975860, to accommodate national keyboard layouts where "`" might be hard to produce;


# 9efa1fdf 15-Apr-2014 wenzelm <none@none>

clarified abbreviations for cartouche delimiters, to work in any context;


# 4244870c 06-Apr-2014 wenzelm <none@none>

removed abbrev "<-" again (see c771f0fe28d1) due to conflict with important "<->" and "<-->";


# 3e708841 03-Apr-2014 wenzelm <none@none>

more symbol abbrevs, e.g. relevant for list comprehension in HOL/List.thy or HOL/Library/Monad_Syntax.thy;


# a3a498f0 27-Feb-2014 wenzelm <none@none>

more symbol abbrevs to support HOL library maintenance;


# 12a78b44 17-Feb-2014 wenzelm <none@none>

always show PIDE positions as \<here> (0x002302 "House" from DejaVuSansMono);


# c1c23c0c 19-Jan-2014 wenzelm <none@none>

group symbols;


# 42b5b84f 18-Jan-2014 wenzelm <none@none>

support for nested text cartouches;
clarified Symbol.is_symbolic: exclude \<open> and \<close>;


# de17fb4e 15-Jan-2014 wenzelm <none@none>

added \<newline> symbol, which is used for char/string literals in HOL;


# 964c7c0e 31-Aug-2013 wenzelm <none@none>

uniform abbrevs for left/right arrows;


# ad664454 31-Aug-2013 wenzelm <none@none>

more abbrevs according to Isabelle/HOL ASCII replacement syntax;


# 34911b57 30-Aug-2013 wenzelm <none@none>

added common alternative for == (its ambiguity also avoids conflict with ==>);
clarified (= )= [= ]= (like <= >=);
removed * (too intrusive);


# 11a93f40 29-Aug-2013 wenzelm <none@none>

single-letter abbrev does not make sense -- too many candidates;


# 1409e698 29-Aug-2013 wenzelm <none@none>

fewer conflicts -- adhoc resolution of == vs. ==> via unicode (!) image;


# 9ceb54d9 29-Aug-2013 wenzelm <none@none>

more symbol abbrevs;


# be6348ad 29-Aug-2013 wenzelm <none@none>

misc tuning -- reduce conflicts;


# e1563b11 30-Aug-2013 wenzelm <none@none>

more symbol abbrevs, based on ProofGeneral-4.2/isar/isar-unicode-tokens.el and traditional Isabelle/HOL ASCII replacement syntax;


# 81823a5f 28-Aug-2013 wenzelm <none@none>

complete symbols only in backslash forms -- less intrusive editing, greater chance of finding escape sequence in text;
complete words >= 3 characters only;
discontinued short word abbrev "Un" (see also fdd6e68e29d9 and e38e80686ce5);


# bbb047fd 25-Aug-2013 wenzelm <none@none>

discontinued rendering of obsolete \<onesuperior>, \<twosuperior>, \<threesuperior>;


# 5d7d144f 18-Aug-2013 wenzelm <none@none>

discontinued redundant abbreviations -- Isabelle/jEdit provides keyboard shortcuts already;


# 5dc4e02c 13-Aug-2013 wenzelm <none@none>

discontinued special treatment of \<^isub> and \<^isup> in rendering or editor front-end;
document antiquotations: renamed term style "isub" to "sub";


# 2db19af8 24-Nov-2012 wenzelm <none@none>

more robust font for control symbols, to ensure these obscure codepoints are properly rendered;


# c0e1c77d 24-Nov-2012 wenzelm <none@none>

tuned symbol groups;


# f29baa17 24-Nov-2012 wenzelm <none@none>

tuned symbol groups;


# d3ee7d0f 21-Nov-2012 wenzelm <none@none>

clarified symbol groups, despite this traditional arrangement in X-symbol grid;


# aab072f6 20-Nov-2012 wenzelm <none@none>

some grouping of Isabelle symbols, based on X-Symbol grid in PG-3.7.1.1 and a proposal by Fabian Immler;


# 0a374c9a 03-Aug-2012 wenzelm <none@none>

prefer calligrapic \<RR> \<II> over \<Re> \<Im> for "screen" display (NB: official unicode defines only one version of these glyphs, unlike TeX);


# 10087cb5 14-Jan-2012 wenzelm <none@none>

discontinued default rendering for Oheimb's double-space;


# 39fc0220 21-Jun-2011 wenzelm <none@none>

some arrow symbols from DejaVuSansMono for bsub/esub/bsup/esup;


# 45b80e56 20-Jun-2011 wenzelm <none@none>

removed obsolete font specification;


# 7545a54e 19-Jun-2011 wenzelm <none@none>

abbreviations for special control symbols;


# dd08a565 19-Jun-2011 wenzelm <none@none>

some unicode chars for special control symbols;


# ffc184e6 05-Apr-2011 wenzelm <none@none>

more symbol abbrevs;


# a60b74e2 08-Nov-2010 wenzelm <none@none>

avoid clash of \<upharpoonright> vs. \<restriction> (cf. 666ea7e62384 and 3c49dbece0a8);


# f6ac1e9e 31-May-2010 wenzelm <none@none>

tuned abbrevs for long arrows, according to usual ASCII syntax;


# 38132cf2 29-Oct-2009 wenzelm <none@none>

removed slightly exotic symbol abbreviations for now -- achieves a coherent (unique) mapping;
(NB: in principle symbol abbreviations could well be ambigous);


# 9f3cbe63 22-Oct-2009 tbourke <none@none>

Fix a duplicate abbreviation || in etc/symbols.


# 27f4b255 26-Jun-2009 wenzelm <none@none>

tuned abbrevs;


# 959e9dbc 23-Jun-2009 wenzelm <none@none>

fixed abbrev !! for \<And>;


# 66353221 20-Dec-2008 wenzelm <none@none>

removed Ids;


# 4b74c058 24-Aug-2008 wenzelm <none@none>

activated \<A>, \<a>, \<AA>, \<aa>;
disabled \<RR>, \<II> which overlap with codepoints for \<Re>, \<Im>, remapped to unofficial place within Isabelle font;


# b6cfb225 16-Aug-2008 wenzelm <none@none>

tuned abbrevs;


# a38b933e 15-Aug-2008 wenzelm <none@none>

added some abbrevs;
\<euro>: from default font;


# 090a0d36 15-Aug-2008 wenzelm <none@none>

removed redundant "symbol" property;
added "font" propery;
disabled alternative letters (\<A> etc.) for now;


# 6c34afdf 15-Aug-2008 wenzelm <none@none>

Default interpretation of some Isabelle symbols.