src/Pure/Isar/isar_syn.ML
2013-05-17 wenzelm 2013-05-17 renamed 'print_configs' to 'print_options';
2013-05-14 wenzelm 2013-05-14 more antiquotations;
2013-05-13 wenzelm 2013-05-13 option "goals_limit", with more uniform description;
2013-04-23 haftmann 2013-04-23 target-sensitive user-level commands interpretation and sublocale
2013-04-18 wenzelm 2013-04-18 simplifier uses proper Proof.context instead of historic type simpset;
2013-04-10 wenzelm 2013-04-10 more standard module name Axclass (according to file name);
2013-04-09 wenzelm 2013-04-09 discontinued Toplevel.no_timing complication -- also recovers timing of diagnostic commands, e.g. 'find_theorems'; print timing as tracing, to keep it out of the way in Proof General; no timing of control commands, especially relevant for Proof General;
2013-04-09 wenzelm 2013-04-09 just one syntax category "mixfix" -- check structure annotation semantically;
2013-04-05 wenzelm 2013-04-05 tuned signature -- agree with markup terminology;
2013-03-30 wenzelm 2013-03-30 added 'print_defn_rules' command; tuned;
2013-02-28 wenzelm 2013-02-28 discontinued obsolete 'axioms' command;
2013-02-27 wenzelm 2013-02-27 discontinued redundant 'use' command;
2013-01-05 wenzelm 2013-01-05 tuned -- less indirection;
2012-11-26 wenzelm 2012-11-26 tuned command descriptions;
2012-11-26 wenzelm 2012-11-26 refined outer syntax 'help' command;
2012-10-16 wenzelm 2012-10-16 more informative errors for 'also' and 'finally';
2012-10-16 wenzelm 2012-10-16 clarified defer/prefer: more specific errors;
2012-10-16 wenzelm 2012-10-16 more informative errors for 'proof' and 'apply' steps; more Seq.result operations;
2012-09-26 wenzelm 2012-09-26 tuned pretty_locale/print_locale, with more basic pretty_locale_deps based on that; added command 'locale_deps'; graphview prints plain text only -- removed dependency on old Cobra HTML_Panel;
2012-08-29 wenzelm 2012-08-29 command 'use' is legacy;
2012-08-26 wenzelm 2012-08-26 theory def/ref position reports, which enable hyperlinks etc.; more official header command parsing;
2012-08-22 wenzelm 2012-08-22 clarified Parse.path vs. Parse.explode -- prefer errors in proper transaction context;
2012-08-14 wenzelm 2012-08-14 support for 'typ' with explicit sort constraint;
2012-08-02 wenzelm 2012-08-02 more official command specifications, including source position;
2012-08-02 wenzelm 2012-08-02 more antiquotations;
2012-08-02 wenzelm 2012-08-02 more antiquotations;
2012-08-02 wenzelm 2012-08-02 more antiquotations;
2012-08-01 wenzelm 2012-08-01 more standard bootstrapping of Pure outer syntax;
2012-04-10 wenzelm 2012-04-10 static relevance of proof via syntax keywords;
2012-04-01 wenzelm 2012-04-01 more general context command with auxiliary fixes/assumes etc.;
2012-03-21 wenzelm 2012-03-21 more explicit Toplevel.open_target/close_target; replaced 'context_includes' by 'context' 'includes'; tuned command descriptions;
2012-03-21 wenzelm 2012-03-21 optional 'includes' element for long theorem statements; tuned signatures;
2012-03-21 wenzelm 2012-03-21 basic support for nested contexts including bundles; include multiple bundles; renamed "affirm" back to "assert" (cf. c4492c6bf450 which was motivated by obsolete Alice/ML); tuned signatures;
2012-03-20 wenzelm 2012-03-20 basic support for bundled declarations;
2012-03-17 wenzelm 2012-03-17 more precise syntax;
2012-03-16 wenzelm 2012-03-16 eliminated odd 'finalconsts' / Theory.add_finals;
2012-03-16 wenzelm 2012-03-16 more abstract heading level;
2012-03-16 wenzelm 2012-03-16 outer syntax command definitions based on formal command_spec derived from theory header declarations;
2012-03-16 wenzelm 2012-03-16 define keywords early when processing the theory header, before running the body commands;
2012-03-15 wenzelm 2012-03-15 declare command keywords via theory header, including strict checking outside Pure;
2012-03-15 wenzelm 2012-03-15 declare minor keywords via theory header;
2012-03-15 wenzelm 2012-03-15 some support for outer syntax keyword declarations within theory header; more uniform Thy_Header.header as argument for begin_theory etc.;
2012-03-14 wenzelm 2012-03-14 source positions for locale and class expressions;
2011-12-13 wenzelm 2011-12-13 tuned;
2011-11-20 wenzelm 2011-11-20 'lemmas' / 'theorems' commands allow 'for' fixes and standardize the result before storing;
2011-11-14 wenzelm 2011-11-14 pass positions for named targets, for formal links in the document model;
2011-10-13 wenzelm 2011-10-13 discontinued obsolete 'types' command;
2011-08-13 wenzelm 2011-08-13 less verbosity in batch mode -- spam reduction and notable performance improvement; clarified Proof_Display.print_consts;
2011-08-13 wenzelm 2011-08-13 simplified Toplevel.init_theory: discontinued special name argument;
2011-08-13 wenzelm 2011-08-13 simplified Toplevel.init_theory: discontinued special master argument;
2011-07-23 wenzelm 2011-07-23 defer evaluation of Scan.message, for improved performance in the frequent situation where failure is handled later (e.g. via ||);
2011-07-12 wenzelm 2011-07-12 added Parse.properties (again) -- allow empty list like Parse_Value.properties but unlike Parse.properties of ef86de9c98aa;
2011-06-07 blanchet 2011-06-07 fixed typo in legacy feature message
2011-05-15 wenzelm 2011-05-15 optional description for 'attribute_setup' and 'method_setup';
2011-04-27 wenzelm 2011-04-27 more precise positions via binding;
2011-04-23 wenzelm 2011-04-23 proper binding/report of defined simprocs; tuned signature;
2011-04-17 wenzelm 2011-04-17 report Name_Space.declare/define, relatively to context; added "global" variants of context-dependent declarations;
2011-04-16 wenzelm 2011-04-16 prefer local name spaces; tuned signatures; tuned;
2011-04-09 wenzelm 2011-04-09 some position reports for 'translations';
2011-04-08 wenzelm 2011-04-08 notation: proper markup for type constructor / constant;