src/Pure/Isar/method.ML
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;
2006-01-29 wenzelm 2006-01-29 method (un)folded: option '(raw)';
2006-01-28 wenzelm 2006-01-28 (un)fold: support object-level rewrites;
2006-01-21 wenzelm 2006-01-21 simplified type attribute;
2006-01-19 wenzelm 2006-01-19 setup: theory -> theory;
2006-01-10 wenzelm 2006-01-10 generic attributes; tuned;
2005-12-22 wenzelm 2005-12-22 conjunction_tac: single goal;
2005-12-16 haftmann 2005-12-16 re-arranged tuples (theory * 'a) to ('a * theory) in Pure
2005-11-30 wenzelm 2005-11-30 method 'fact': SIMPLE_METHOD, i.e. insert facts;
2005-11-22 wenzelm 2005-11-22 moved multi_resolve(s) to drule.ML; cases_tactic;
2005-11-10 wenzelm 2005-11-10 renamed Thm.cgoal_of to Thm.cprem_of;
2005-10-28 wenzelm 2005-10-28 added fact method; accomodate simplified Thm.lift_rule;
2005-10-15 wenzelm 2005-10-15 added primitive_text, succeed_text;
2005-10-04 wenzelm 2005-10-04 minor tweaks for Poplog/ML;
2005-09-22 nipkow 2005-09-22 renamed "rules" to "iprover"
2005-09-20 haftmann 2005-09-20 slight adaptions to library changes
2005-09-15 wenzelm 2005-09-15 TableFun/Symtab: curried lookup and update;
2005-09-13 wenzelm 2005-09-13 added cheating, sorry_text (from skip_proofs.ML); added method_setup (from isar_thy.ML);
2005-09-08 haftmann 2005-09-08 introduces some modern-style AList operations
2005-09-01 wenzelm 2005-09-01 curried_lookup/update;
2005-08-18 wenzelm 2005-08-18 moved before proof.ML; added FINDGOAL/HEADGOAL (from proof.ML); added type method (from proof.ML); moved proof refinement etc. to proof.ML; tuned;