doc-src/IsarRef/Thy/document/Inner_Syntax.tex
2012-02-17 wenzelm 2012-02-17 simplified configuration options for syntax ambiguity;
2012-02-16 wenzelm 2012-02-16 simplified configuration options for syntax ambiguity;
2012-02-15 wenzelm 2012-02-15 clarified outer syntax "constdecl", which is only local to some rail diagrams;
2012-02-15 wenzelm 2012-02-15 renamed "xstr" to "str_token";
2012-02-07 wenzelm 2012-02-07 tuned;
2012-02-07 wenzelm 2012-02-07 updated examples for syntax translations;
2012-02-05 wenzelm 2012-02-05 updated section on raw syntax; misc tuning;
2012-02-05 wenzelm 2012-02-05 updated section about syntax ambiguity;
2012-02-04 wenzelm 2012-02-04 updated/unified section on mixfix annotations;
2012-02-04 wenzelm 2012-02-04 tuned;
2012-02-04 wenzelm 2012-02-04 more on explicit notation;
2012-02-04 wenzelm 2012-02-04 more accurate Pure grammar;
2012-02-04 wenzelm 2012-02-04 more refs;
2012-02-04 wenzelm 2012-02-04 simplified mixfix (NB: infix is no longer required separately);
2012-02-02 wenzelm 2012-02-02 updated section on print modes;
2012-02-02 wenzelm 2012-02-02 clarified syntax section structure;
2011-12-01 wenzelm 2011-12-01 renamed inner syntax categories "num" to "num_token" and "xnum" to "xnum_token";
2011-06-04 wenzelm 2011-06-04 tuned secref (still dangling);
2011-05-05 wenzelm 2011-05-05 tuned some syntax names;
2011-05-03 wenzelm 2011-05-03 more conventional naming scheme: names_long, names_short, names_unique;
2011-05-03 wenzelm 2011-05-03 updated generated files;
2011-05-03 wenzelm 2011-05-03 updated configuration options -- no ML here;
2011-05-03 wenzelm 2011-05-03 formal Base theory;
2011-05-02 wenzelm 2011-05-02 modernized rail diagrams using @{rail} antiquotation;
2011-04-16 wenzelm 2011-04-16 Name_Space: proper configuration options long_names, short_names, unique_names instead of former unsynchronized references;
2011-04-07 wenzelm 2011-04-07 constant =?= no longer exists (cf. 8c09e1fa24a7);
2011-04-06 wenzelm 2011-04-06 typed_print_translation: discontinued show_sorts argument;
2010-12-17 wenzelm 2010-12-17 replaced command 'nonterminals' by slightly modernized version 'nonterminal';
2010-12-02 wenzelm 2010-12-02 configuration option "show_abbrevs" supersedes print mode "no_abbrevs", with inverted meaning;
2010-11-08 wenzelm 2010-11-08 updated generated files;
2010-10-29 wenzelm 2010-10-29 eliminated obsolete \_ escapes in rail environments;
2010-09-10 wenzelm 2010-09-10 updated config options;
2010-09-06 wenzelm 2010-09-06 discontinued obsolete ProofContext.prems_limit; simplified command setup for 'pr' etc.;
2010-09-05 wenzelm 2010-09-05 turned show_brackets into proper configuration option; Sign.certify/type_check: dropped Syntax.pp_show_brackets, which is hard to hold up due to Pretty.pp and not even present in the regular end-user type check;
2010-09-05 wenzelm 2010-09-05 turned show_sorts/show_types into proper configuration options;
2010-09-04 wenzelm 2010-09-04 updated configuration options;
2010-09-03 wenzelm 2010-09-03 turned show_consts into proper configuration option;
2010-09-02 wenzelm 2010-09-02 turned show_question_marks into proper configuration option; show_question_marks only affects regular type/term pretty printing, not raw Term.string_of_vname; tuned;
2010-05-08 wenzelm 2010-05-08 discontinued Pretty.setdepth, which appears to be largely unused, but can disrupt important markup if enabled accidentally;
2010-05-08 wenzelm 2010-05-08 unified/simplified Pretty.margin_default; discontinued special Pretty.setmargin etc; explicit margin argument for Pretty.string_of_margin etc.;
2010-04-29 wenzelm 2010-04-29 allow concrete syntax for local entities within a proof body, either via regular mixfix annotations to 'fix' etc. or the separate 'write' command;
2010-03-01 wenzelm 2010-03-01 updated generated files;
2010-02-24 wenzelm 2010-02-24 allow general mixfix syntax for type constructors;
2009-10-01 wenzelm 2009-10-01 updated generated files;
2009-03-09 wenzelm 2009-03-09 markup antiquotation options; more correct references to external manuals;
2009-03-04 blanchet 2009-03-04 Merge.
2009-03-04 blanchet 2009-03-04 Merge.
2009-02-26 wenzelm 2009-02-26 updated generated files;
2009-02-15 wenzelm 2009-02-15 updated generated files;
2008-12-23 wenzelm 2008-12-23 updated generated file;
2008-11-20 wenzelm 2008-11-20 updated generated files;
2008-11-13 wenzelm 2008-11-13 separate chapter "Inner syntax --- the term language";