src/Pure/Isar/method.ML
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;
2005-07-19 wenzelm 2005-07-19 Logic.incr_tvar;
2005-06-20 wenzelm 2005-06-20 refl_tac: avoid failure of unification, i.e. confusing trace msg; get_thm(s): Name;
2005-06-17 wenzelm 2005-06-17 (RAW_)METHOD_CASES: RuleCases.tactic; accomodate change of TheoryDataFun;
2005-06-09 wenzelm 2005-06-09 meths: NameSpace.table;
2005-05-31 wenzelm 2005-05-31 renamed cond_extern to extern; Sign.declare_name replaces NameSpace.extend; (RAW_)METHOD_CASES: RuleCases.T option;
2005-05-17 wenzelm 2005-05-17 tuned;
2005-04-23 wenzelm 2005-04-23 removed structure PureIsar;
2005-04-21 wenzelm 2005-04-21 superceded by Pure.thy and CPure.thy;
2005-04-21 berghofe 2005-04-21 Adapted to new interface of instantiation and unification / matching functions.
2005-04-13 wenzelm 2005-04-13 *** MESSAGE REFERS TO PREVIOUS VERSION *** type src = Args.src; Drule.add_used;
2005-04-13 wenzelm 2005-04-13 *** empty log message ***
2005-03-04 skalberg 2005-03-04 Removed practically all references to Library.foldr.
2005-03-03 skalberg 2005-03-03 Move towards standard functions.
2005-02-13 skalberg 2005-02-13 Deleted Library.option type.
2005-01-24 berghofe 2005-01-24 Specific theorems in a named list of theorems can now be referred to via indices (type thmref).
2004-06-21 kleing 2004-06-21 Merged in license change from Isabelle2004
2004-05-07 wenzelm 2004-05-07 tuned;
2004-04-02 ballarin 2004-04-02 Experimental command for instantiation of locales in proof contexts: instantiate <label>: <loc>
2003-09-30 ballarin 2003-09-30 Improvements to Isar/Locales: premises generated by "includes" elements changed. Bugfix "unify_frozen".
2003-08-29 ballarin 2003-08-29 Methods rule_tac etc support static (Isar) contexts.
2002-10-17 paulson 2002-10-17 fixing the cut_tac method to work when there are no instantiations and the supplied theorems have premises
2002-01-21 wenzelm 2002-01-21 full_atomize;
2001-12-06 wenzelm 2001-12-06 tuned;
2001-12-05 wenzelm 2001-12-05 simple version of 'intro' and 'elim' method; use ContextRules.find_rules;
2001-12-04 wenzelm 2001-12-04 rules_tac: SELECT_GOAL!!; tuned;
2001-12-03 wenzelm 2001-12-03 renamed rule_context.ML to context_rules.ML;