src/Pure/ML/ml_thms.ML
2017-06-12 wenzelm 2017-06-12 more markup for HTML rendering;
2016-05-23 wenzelm 2016-05-23 embedded content may be delimited via cartouches;
2016-04-07 wenzelm 2016-04-07 simplified default print_depth: context is usually available, in contrast to 0d295e339f52;
2016-04-05 wenzelm 2016-04-05 clarified modules -- simplified bootstrap;
2015-12-09 wenzelm 2015-12-09 clarified type Token.src: plain token list, with usual implicit value assignment; clarified type Token.name_value, notably for head of Token.src; clarified Attrib/Method check_src vs. parser;
2014-12-10 wenzelm 2014-12-10 more careful handling of auxiliary environment structure -- allow nested ML evaluation;
2014-12-08 wenzelm 2014-12-08 expand ML cartouches to Input.source; tuned signature;
2014-11-01 wenzelm 2014-11-01 clarified syntax -- avoid overlap with command category;
2014-08-25 wenzelm 2014-08-25 tuned signature;
2014-08-22 wenzelm 2014-08-22 tuned whitespace;
2014-08-21 wenzelm 2014-08-21 tuned signature -- define some elementary operations earlier;
2014-08-19 wenzelm 2014-08-19 tuned signature -- moved type src to Token, without aliases;
2014-03-27 wenzelm 2014-03-27 redirect ML_Compiler reports more directly: only the (big) parse tree report is deferred via Execution.print (NB: this does not work for asynchronous "diag" commands); more explicit ML_Compiler.flags;
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-18 wenzelm 2014-03-18 tuned signature -- rearranged modules;
2014-03-12 wenzelm 2014-03-12 tuned signature -- clarified module name;
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-03-08 wenzelm 2014-03-08 modernized Attrib.check_name/check_src similar to methods (see also a989bdaf8121); proper context for global data; tuned signature;
2014-03-05 wenzelm 2014-03-05 clarified init_assignable: make double-sure that initial values are reset; more systematic reports for Args.syntax: indicate Args.$$$ quasi-keywords and suppress confusing completion of single symbols like ":", "|", "?";
2014-02-28 wenzelm 2014-02-28 more explicit method reports; avoid combinator parsers with observable effect -- unreliable due to backtracking (Scan.FAIL) and incremental input (Scan.MORE);
2014-02-26 wenzelm 2014-02-26 tuned;
2014-02-26 wenzelm 2014-02-26 method language markup, e.g. relevant to prevent outer keyword completion;
2014-02-16 wenzelm 2014-02-16 prefer user-space tool within Pure.thy;
2014-02-16 wenzelm 2014-02-16 more markup;
2014-01-22 wenzelm 2014-01-22 tuned signature;
2013-12-31 wenzelm 2013-12-31 proper context for norm_hhf and derived operations; clarified tool context in some boundary cases;
2013-08-23 wenzelm 2013-08-23 added Theory.setup convenience;
2013-08-23 wenzelm 2013-08-23 clarified type ML_Context.antiq: context parser maintains compilation context, declaration is applied to final context; subtle change of semantics of ML_Context.add_antiq: need to avoid accidental update of context due to concrete syntax parser (cf. Scan.pass);
2013-08-23 wenzelm 2013-08-23 tuned signature;
2012-08-12 wenzelm 2012-08-12 tuned;
2012-08-12 wenzelm 2012-08-12 more direct embedding of abstract thm values into the ML environment -- avoidance of repeated ML_Thms.the_thm(s) considerably reduces compilation time for Poly/ML 5.4.x;
2012-08-11 wenzelm 2012-08-11 faster compilation of ML with antiquotations: static ML_context is bound once in auxiliary structure Isabelle;
2012-04-27 wenzelm 2012-04-27 clarified signature;
2011-11-19 wenzelm 2011-11-19 added ML antiquotation @{attributes};
2011-10-19 wenzelm 2011-10-19 proper source positions for @{lemma};
2011-06-27 wenzelm 2011-06-27 ML antiquotations are managed as theory data, with proper name space and entity markup; clarified Name_Space.check;
2011-04-16 wenzelm 2011-04-16 modernized structure Proof_Context;
2011-01-09 wenzelm 2011-01-09 reverted 08240feb69c7 -- breaks positions of reports;
2010-12-21 wenzelm 2010-12-21 more robust ML antiquotations -- allow original tokens without adjacent whitespace;
2010-05-31 wenzelm 2010-05-31 modernized some structure names, keeping a few legacy aliases;
2010-05-15 wenzelm 2010-05-15 refer directly to structure Keyword and Parse; eliminated old-style structure aliases K and P;
2010-04-25 wenzelm 2010-04-25 modernized naming conventions of main Isar proof elements;
2010-02-07 wenzelm 2010-02-07 simplified interface for ML antiquotations, struct_name is always "Isabelle";
2009-11-15 wenzelm 2009-11-15 eliminated obsolete thm position tags;
2009-11-08 wenzelm 2009-11-08 adapted Generic_Data, Proof_Data; tuned;
2009-03-04 wenzelm 2009-03-04 ML antiquotation @{lemma}: allow 'and' list, proper simultaneous type-checking;
2009-01-21 wenzelm 2009-01-21 removed Ids;
2008-08-14 wenzelm 2008-08-14 ML_Context.add_antiq: pass position; @{lemma}: set source position;
2008-08-09 wenzelm 2008-08-09 unified Args.T with OuterLex.token, renamed some operations;
2008-07-10 wenzelm 2008-07-10 @{lemma}: allow terminal method, close derivation unless (open) mode is given;
2008-06-28 wenzelm 2008-06-28 Isar theorem values within ML.