src/HOL/Prolog/prolog.ML
2015-07-18 wenzelm 2015-07-18 prefer tactics with explicit context;
2015-03-19 wenzelm 2015-03-19 more position information;
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-04-08 wenzelm 2014-04-08 more uniform ML/document antiquotations;
2014-03-21 wenzelm 2014-03-21 more qualified names;
2014-01-26 wenzelm 2014-01-26 tuned signature;
2014-01-25 wenzelm 2014-01-25 explicit eigen-context for attributes "where", "of", and corresponding read_instantiate, instantiate_tac;
2013-05-30 wenzelm 2013-05-30 tuned;
2013-05-20 wenzelm 2013-05-20 proper run-time context;
2013-05-16 wenzelm 2013-05-16 more system options as context-sensitive config options;
2012-02-14 wenzelm 2012-02-14 more conventional tactic setup;
2012-01-09 wenzelm 2012-01-09 prefer antiquotations;
2011-11-27 wenzelm 2011-11-27 more antiquotations;
2011-11-24 wenzelm 2011-11-24 modernized some old-style infix operations, which were left over from the time of ML proof scripts;
2010-09-03 wenzelm 2010-09-03 pretty_goals: turned some global references and function arguments into configuration options (goals_limit = 10, goals_total = true, show_main_goal = false) depending on the context;
2010-08-27 wenzelm 2010-08-27 expanded some aliases from structure Unsynchronized;
2010-08-27 haftmann 2010-08-27 formerly unnamed infix conjunction and disjunction now named HOL.conj and HOL.disj
2010-08-26 haftmann 2010-08-26 formerly unnamed infix impliciation now named HOL.implies
2010-08-19 haftmann 2010-08-19 more antiquotations
2010-08-19 haftmann 2010-08-19 use antiquotations for remaining unqualified constants in HOL
2010-05-15 wenzelm 2010-05-15 less pervasive names from structure Thm;
2010-02-19 wenzelm 2010-02-19 renamed Simplifier.theory_context to Simplifier.global_context to emphasize that this is not the real thing;
2009-10-15 wenzelm 2009-10-15 replaced String.concat by implode; replaced String.concatWith by space_implode; replaced (Seq.flat o Seq.map) by Seq.maps; replaced List.mapPartial by map_filter; replaced List.concat by flat; replaced (flat o map) by maps, which produces less garbage;
2009-09-29 wenzelm 2009-09-29 explicit indication of Unsynchronized.ref;
2009-07-30 wenzelm 2009-07-30 qualified Subgoal.FOCUS;
2009-07-30 wenzelm 2009-07-30 FOCUS_PREMS as full replacement for METAHYPS, where the conclusion may still contain schematic variables;
2009-07-28 wenzelm 2009-07-28 eliminated METAHYPS;
2009-07-15 wenzelm 2009-07-15 more antiquotations;
2008-06-16 wenzelm 2008-06-16 pervasive RuleInsts;
2008-06-16 wenzelm 2008-06-16 ptac/prolog_tac: proper context;
2008-06-11 wenzelm 2008-06-11 Drule.read_instantiate;
2006-11-20 wenzelm 2006-11-20 HOL-Prolog: converted legacy ML scripts;