src/Pure/Isar/method.ML
2009-03-01 wenzelm 2009-03-01 use long names for old-style fold combinators;
2009-02-28 wenzelm 2009-02-28 moved generic intuitionistic prover to src/Tools/intuitionistic.ML;
2009-02-11 kleing 2009-02-11 FindTheorems: add solves feature; tidy up const name subsettin; patch by Timothy Bourke
2009-01-01 wenzelm 2009-01-01 assumption/close: discontinued implicit prems;
2008-12-05 haftmann 2008-12-05 removed Table.extend, NameSpace.extend_table
2008-08-09 wenzelm 2008-08-09 unified Args.T with OuterLex.token, renamed some operations; removed obsolete parse_args (cf. parse);
2008-08-06 wenzelm 2008-08-06 report markup;
2008-08-04 wenzelm 2008-08-04 tuned signature; eliminated obsolete pervasives;
2008-06-28 wenzelm 2008-06-28 replaced simple_text by fully-featured parse_args;
2008-06-16 wenzelm 2008-06-16 renamed rename_params_tac to rename_tac;
2008-06-16 wenzelm 2008-06-16 ML tactic: do not abstract over context again;
2008-05-14 wenzelm 2008-05-14 added intern, defined;
2008-04-29 haftmann 2008-04-29 added lemma antiquotation
2008-03-28 wenzelm 2008-03-28 ml_tactic: non-critical version via proof data and thread data;
2008-03-28 wenzelm 2008-03-28 Context.>> : operate on Context.generic;
2008-03-28 wenzelm 2008-03-28 reorganized signature of ML_Context;
2008-03-27 wenzelm 2008-03-27 eliminated delayed theory setup
2008-03-26 wenzelm 2008-03-26 adapted to Context.thread_data interface;
2008-03-24 wenzelm 2008-03-24 ML runtime compilation: pass position, tuned signature;
2008-03-15 wenzelm 2008-03-15 tuned messages;
2008-01-24 wenzelm 2008-01-24 improved apply: handle thread position, apply to context here; replaced ContextPosition by Position.thread_position;
2007-12-18 wenzelm 2007-12-18 named some critical sections;
2007-11-02 haftmann 2007-11-02 generic tactic Method.intros_tac
2007-08-01 wenzelm 2007-08-01 tuned;
2007-07-28 wenzelm 2007-07-28 tuned;
2007-07-27 wenzelm 2007-07-27 method section scanners: added [[declaration]] syntax, ignore sid-effects of thms;
2007-07-23 wenzelm 2007-07-23 eliminated transform_failure (to avoid critical section for main transactions);
2007-07-23 wenzelm 2007-07-23 marked some CRITICAL sections (for multithreading);
2007-07-08 wenzelm 2007-07-08 replaced exception TableFun/GraphFun.DUPS by TableFun/GraphFun.DUP;
2007-07-05 wenzelm 2007-07-05 renamed ObjectLogic.atomize_tac to ObjectLogic.atomize_prems_tac;
2007-07-05 wenzelm 2007-07-05 avoid polymorphic equality;
2007-06-19 wenzelm 2007-06-19 added raw_tactic;
2007-06-14 wenzelm 2007-06-14 method assumption: uniform treatment of prems as legacy feature;
2007-06-13 wenzelm 2007-06-13 Basic text: include position; assumption/close: refer to non-atomic assumptions as well, implicit use of prems now considered legacy feature;
2007-05-31 wenzelm 2007-05-31 simplified/unified list fold;
2007-05-24 haftmann 2007-05-24 tuned Pure/General/name_space.ML
2007-05-07 wenzelm 2007-05-07 simplified DataFun interfaces;
2007-04-04 wenzelm 2007-04-04 tuned comment;
2007-01-20 wenzelm 2007-01-20 ML tactic: proper context for compile and runtime;
2007-01-19 wenzelm 2007-01-19 removed obsolete Method; added parse (from outer_parse.ML); moved ML context stuff to from Context to ML_Context; tactic: no need to rebind thm/thms;
2007-01-19 wenzelm 2007-01-19 adapted ML context operations;
2006-12-30 wenzelm 2006-12-30 removed conditional combinator;
2006-12-18 haftmann 2006-12-18 switched argument order in *.syntax lifters
2006-12-07 wenzelm 2006-12-07 reorganized structure Goal vs. Tactic;
2006-11-29 wenzelm 2006-11-29 renamed SIMPLE_METHOD' to SIMPLE_METHOD''; added simple version of SIMPLE_METHOD';
2006-11-29 wenzelm 2006-11-29 COMP_INCR;
2006-08-03 wenzelm 2006-08-03 moved bires_inst_tac etc. to rule_insts.ML;
2006-08-02 wenzelm 2006-08-02 normalized Proof.context/method type aliases;
2006-07-27 wenzelm 2006-07-27 moved basic assumption operations from structure ProofContext to Assumption;
2006-07-12 wenzelm 2006-07-12 removed duplicate of Tactic.make_elim_preserve;
2006-07-06 wenzelm 2006-07-06 added method_i and Source_i;
2006-06-05 wenzelm 2006-06-05 assm_tac: try rule termI;
2006-04-27 wenzelm 2006-04-27 tuned basic list operators (flat, maps, map_filter);
2006-03-21 wenzelm 2006-03-21 moved gen_eq_set to library.ML;
2006-03-04 wenzelm 2006-03-04 text: added SelectGoals;
2006-02-15 wenzelm 2006-02-15 removed distinct, renamed gen_distinct to distinct;
2006-02-10 wenzelm 2006-02-10 syntax: Context.generic;
2006-02-06 wenzelm 2006-02-06 tuned;
2006-02-03 wenzelm 2006-02-03 canonical member/insert/merge;
2006-01-31 wenzelm 2006-01-31 (un)fold: removed '(raw)' option;