src/HOL/Statespace/state_space.ML
2015-11-14 haftmann 2015-11-14 separate ML module for interpretation
2015-11-09 wenzelm 2015-11-09 uniform mandatory qualifier for all locale expressions, including 'statespace' parent; removed obsolete '!' syntax;
2015-09-09 wenzelm 2015-09-09 simplified simproc programming interfaces;
2015-07-18 wenzelm 2015-07-18 prefer tactics with explicit context;
2015-06-01 wenzelm 2015-06-01 clarified context;
2015-04-06 wenzelm 2015-04-06 @{command_spec} is superseded by @{command_keyword};
2015-04-01 wenzelm 2015-04-01 imitate old "intern" semantics for the sake of outdated/unmaintained code, notably relevant for Simpl;
2015-03-04 wenzelm 2015-03-04 tuned signature -- prefer qualified names;
2015-02-10 wenzelm 2015-02-10 proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.; occasionally clarified use of context;
2014-06-06 haftmann 2014-06-06 dropped obscure and unused ad-hoc before_exit hook for named targets
2014-03-07 wenzelm 2014-03-07 removed dead code;
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;
2012-11-26 wenzelm 2012-11-26 tuned command descriptions;
2012-10-17 wenzelm 2012-10-17 more method position information, notably finished_pos after end of previous text;
2012-10-16 wenzelm 2012-10-16 more proof method text position information;
2012-10-10 wenzelm 2012-10-10 more explicit namespace prefix for 'statespace' -- duplicate facts;
2012-08-09 wenzelm 2012-08-09 tuned signature;
2012-03-16 wenzelm 2012-03-16 outer syntax command definitions based on formal command_spec derived from theory header declarations;
2012-03-15 wenzelm 2012-03-15 prefer formally checked @{keyword} parser;
2012-03-14 wenzelm 2012-03-14 locale expressions without source positions;
2011-12-02 wenzelm 2011-12-02 eliminated some legacy operations;
2011-11-28 wenzelm 2011-11-28 tuned messages;
2011-11-06 wenzelm 2011-11-06 misc tuning and modernization; more antiquotations;
2011-11-06 wenzelm 2011-11-06 tuned;
2011-10-28 wenzelm 2011-10-28 uniform Local_Theory.declaration with explicit params;
2011-08-10 wenzelm 2011-08-10 old term operations are legacy;
2011-06-29 wenzelm 2011-06-29 simplified/unified Simplifier.mk_solver;
2011-06-09 wenzelm 2011-06-09 discontinued Name.variant to emphasize that this is old-style / indirect;
2011-06-08 wenzelm 2011-06-08 more robust exception pattern General.Subscript;
2011-04-27 wenzelm 2011-04-27 reorganized fixes as specialized (global) name space;
2011-04-16 wenzelm 2011-04-16 proper subgoal addressing via SUBGOAL/CSUBGOAL -- assuming these tactics did not handle Subscript in any special way; tuned;
2011-04-16 wenzelm 2011-04-16 eliminated old List.nth; tuned;
2011-04-16 wenzelm 2011-04-16 modernized structure Proof_Context;
2011-04-08 wenzelm 2011-04-08 discontinued special treatment of structure Mixfix; eliminated slightly odd no_syn convenience;
2011-04-06 wenzelm 2011-04-06 separate structure Term_Position; dismantled remains of structure Type_Ext;
2011-03-22 wenzelm 2011-03-22 statespace syntax: strip positions -- type constraints are unexpected here;
2011-01-16 wenzelm 2011-01-16 added before_exit continuation for named targets (locale, class etc.), e.g. for final check/cleanup as in VC management;
2011-01-08 wenzelm 2011-01-08 misc tuning and comments based on review of Theory_Data, Proof_Data, Generic_Data usage;
2010-12-18 ballarin 2010-12-18 Add mixins to sublocale command.
2010-09-05 wenzelm 2010-09-05 turned show_sorts/show_types into proper configuration options;
2010-08-28 haftmann 2010-08-28 formerly unnamed infix equality now named HOL.eq
2010-08-27 wenzelm 2010-08-27 eliminated broken Output.no_warnings_CRITICAL -- context visibility does the job; modernized attribute setup;
2010-08-25 wenzelm 2010-08-25 renamed Simplifier.simproc(_i) to Simplifier.simproc_global(_i) to emphasize that this is not the real thing;
2010-08-19 haftmann 2010-08-19 tuned quotes
2010-08-19 haftmann 2010-08-19 use antiquotations for remaining unqualified constants in HOL
2010-08-12 haftmann 2010-08-12 Named_Target.init: empty string represents theory target
2010-08-11 haftmann 2010-08-11 renamed Theory_Target to the more appropriate Named_Target
2010-05-27 wenzelm 2010-05-27 renamed structure PrintMode to Print_Mode, keeping the old name as legacy alias for some time;
2010-05-17 wenzelm 2010-05-17 prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax; eliminated old-style structure aliases K = Keyword, P = Parse;
2010-05-17 wenzelm 2010-05-17 tuned;
2010-05-05 haftmann 2010-05-05 farewell to old-style mem infixes -- type inference in situations with mem_int and mem_string should provide enough information to resolve the type of (op =)
2010-05-03 wenzelm 2010-05-03 renamed ProofContext.init to ProofContext.init_global to emphasize that this is not the real thing;
2010-04-29 wenzelm 2010-04-29 adapted ProofContext.infer_type;
2010-04-15 wenzelm 2010-04-15 inline old Record.read_typ/cert_typ; spelling;
2009-11-13 wenzelm 2009-11-13 modernized structure Local_Theory;
2009-11-10 wenzelm 2009-11-10 modernized structure Theory_Target;
2009-11-08 wenzelm 2009-11-08 adapted Generic_Data, Proof_Data; tuned;
2009-11-05 wenzelm 2009-11-05 adapted LocalTheory.declaration;
2009-10-27 wenzelm 2009-10-27 critical comments;