src/Pure/Pure.thy
2014-05-05 wenzelm 2014-05-05 support print operations as asynchronous query;
2014-04-29 wenzelm 2014-04-29 suppress slightly odd completions of "real";
2014-04-19 wenzelm 2014-04-19 added command 'SML_export' and 'SML_import' for exchange of toplevel bindings;
2014-03-25 wenzelm 2014-03-25 added command 'SML_file' for Standard ML without Isabelle/ML add-ons;
2014-03-18 wenzelm 2014-03-18 clarified modules; more antiquotations for antiquotations;
2014-03-12 wenzelm 2014-03-12 simplified programming interface to define ML antiquotations -- NB: the transformed context ignores updates of the context parser; added command 'print_ML_antiquotations';
2014-02-26 wenzelm 2014-02-26 suppress completion of obscure keyword, avoid confusion with plain "simp";
2014-02-16 wenzelm 2014-02-16 prefer user-space tool within Pure.thy;
2014-02-10 wenzelm 2014-02-10 discontinued axiomatic 'classes', 'classrel', 'arities';
2014-01-26 wenzelm 2014-01-26 discontinued obsolete attribute "standard";
2014-01-25 wenzelm 2014-01-25 prefer self-contained user-space tool;
2014-01-25 wenzelm 2014-01-25 define basic attributes in user-space Pure.thy -- which provides better hyperlinks and may serve as example;
2014-01-17 wenzelm 2014-01-17 prefer user-space tool within Pure.thy;
2013-12-12 wenzelm 2013-12-12 skeleton for Simplifier trace by Lars Hupel;
2013-09-18 wenzelm 2013-09-18 moved module into plain Isabelle/ML user space;
2013-09-11 wenzelm 2013-09-11 more explicit indication of 'done' as proof script element;
2013-09-02 wenzelm 2013-09-02 more explicit indication of 'guess' as improper Isar (aka "script") element;
2013-07-07 wenzelm 2013-07-07 discontinued command 'print_drafts';
2013-06-25 wenzelm 2013-06-25 recover command tags from 4cf3f6153eb8 -- important for document preparation;
2013-06-24 wenzelm 2013-06-24 improved "isabelle keywords" and "isabelle update_keywords" based on Isabelle/Scala, without requiring to build sessions first; tuned signature;
2013-06-24 wenzelm 2013-06-24 back to keyword 'pr' :: diag as required for ProofGeneral command line -- reject this TTY command in Isabelle/jEdit by other means;
2013-06-24 wenzelm 2013-06-24 more formal ProofGeneral command setup within theory Pure; consider 'ProofGeneral.pr' as control command as well;
2013-06-23 wenzelm 2013-06-23 proper diagnostic command 'print_state';
2013-05-25 wenzelm 2013-05-25 syntax translations always depend on context;
2013-05-17 wenzelm 2013-05-17 renamed 'print_configs' to 'print_options';
2013-05-15 wenzelm 2013-05-15 moved files;
2013-05-15 wenzelm 2013-05-15 maintain ProofGeneral preferences within ProofGeneral module; initialize Isabelle/Pure preferences within normal user space (with antiquotations); tuned;
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-02-27 wenzelm 2013-02-27 discontinued obsolete 'uses' within theory header;
2013-02-25 wenzelm 2013-02-25 discontinued pointless command category "thy_schematic_goal" -- this is checked dynamically;
2013-02-25 wenzelm 2013-02-25 reconsider 'pretty_setmargin' as "control" command (instead of "diag") -- it is stateful and Proof General legacy;
2013-02-19 wenzelm 2013-02-19 back to non-schematic 'sublocale' and 'interpretation' (despite df8fc0567a3d) for more potential parallelism;
2012-12-19 nipkow 2012-12-19 removed odd associativity of ==
2012-11-19 wenzelm 2012-11-19 alternative completion for outer syntax keywords;
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-26 wenzelm 2012-08-26 entity markup for theory Pure, to enable hyperlinks etc.;
2012-08-22 wenzelm 2012-08-22 prefer ML_file over old uses;
2012-08-02 wenzelm 2012-08-02 more official command specifications, including source position;
2012-08-01 wenzelm 2012-08-01 more standard bootstrapping of Pure outer syntax;
2012-08-01 wenzelm 2012-08-01 more standard bootstrapping of Pure.thy;
2009-01-21 wenzelm 2009-01-21 removed Ids;
2008-11-20 wenzelm 2008-11-20 Pure syntax: more coherent treatment of aprop, permanent TERM and &&&;
2008-10-28 ballarin 2008-10-28 Removed 'includes meta_term_syntax' and 'includes meta_conjunction_syntax'.
2008-07-25 haftmann 2008-07-25 dropped locale (open)
2008-05-18 wenzelm 2008-05-18 converted to regular application syntax;
2008-04-07 wenzelm 2008-04-07 prefer plain ASCII here;
2008-04-07 wenzelm 2008-04-07 added swap_params;
2008-03-27 wenzelm 2008-03-27 eliminated delayed theory setup
2008-03-27 wenzelm 2008-03-27 reduced to theory body (cf. OuterSyntax.process_file);
2007-07-17 wenzelm 2007-07-17 moved print_translations from Pure.thy to Syntax/syn_trans.ML;
2007-06-20 nipkow 2007-06-20 added meta_impE
2007-05-11 wenzelm 2007-05-11 tuned proofs;
2006-12-02 wenzelm 2006-12-02 meta_term_syntax: proper operation on untyped preterms;
2006-12-02 wenzelm 2006-12-02 added some support for embedded terms;
2006-09-19 wenzelm 2006-09-19 revert to previous version;
2006-09-19 haftmann 2006-09-19 (void)
2006-06-06 wenzelm 2006-06-06 removed Toplevel.debug;
2006-06-06 ballarin 2006-06-06 Improved parameter management of locales.