src/Pure/Isar/method.ML
2006-01-19 ago setup: theory -> theory;
2006-01-10 ago generic attributes;
2005-12-22 ago conjunction_tac: single goal;
2005-12-16 ago re-arranged tuples (theory * 'a) to ('a * theory) in Pure
2005-11-30 ago method 'fact': SIMPLE_METHOD, i.e. insert facts;
2005-11-22 ago moved multi_resolve(s) to drule.ML;
2005-11-10 ago renamed Thm.cgoal_of to Thm.cprem_of;
2005-10-28 ago added fact method;
2005-10-15 ago added primitive_text, succeed_text;
2005-10-04 ago minor tweaks for Poplog/ML;
2005-09-22 ago renamed "rules" to "iprover"
2005-09-20 ago slight adaptions to library changes
2005-09-15 ago TableFun/Symtab: curried lookup and update;
2005-09-13 ago added cheating, sorry_text (from skip_proofs.ML);
2005-09-08 ago introduces some modern-style AList operations
2005-09-01 ago curried_lookup/update;
2005-08-18 ago moved before proof.ML;
2005-07-19 ago Logic.incr_tvar;
2005-06-20 ago refl_tac: avoid failure of unification, i.e. confusing trace msg;
2005-06-17 ago (RAW_)METHOD_CASES: RuleCases.tactic;
2005-06-09 ago meths: NameSpace.table;
2005-05-31 ago renamed cond_extern to extern;
2005-05-17 ago tuned;
2005-04-23 ago removed structure PureIsar;
2005-04-21 ago superceded by Pure.thy and CPure.thy;
2005-04-21 ago Adapted to new interface of instantiation and unification / matching functions.
2005-04-13 ago *** MESSAGE REFERS TO PREVIOUS VERSION ***
2005-04-13 ago *** empty log message ***
2005-03-04 ago Removed practically all references to Library.foldr.
2005-03-03 ago Move towards standard functions.
2005-02-13 ago Deleted Library.option type.
2005-01-24 ago Specific theorems in a named list of theorems can now be referred to
2004-06-21 ago Merged in license change from Isabelle2004
2004-05-07 ago tuned;
2004-04-02 ago Experimental command for instantiation of locales in proof contexts:
2003-09-30 ago Improvements to Isar/Locales: premises generated by "includes" elements
2003-08-29 ago Methods rule_tac etc support static (Isar) contexts.
2002-10-17 ago fixing the cut_tac method to work when there are no instantiations and the
2002-01-21 ago full_atomize;
2001-12-06 ago tuned;
2001-12-05 ago simple version of 'intro' and 'elim' method;
2001-12-04 ago rules_tac: SELECT_GOAL!!;
2001-12-03 ago renamed rule_context.ML to context_rules.ML;
2001-12-03 ago added "rules" method;
2001-11-29 ago rule context and attributes moved to rule_context.ML;
2001-11-28 ago theory data: removed obsolete finish method;
2001-11-21 ago use tracing function for trace output;
2001-11-19 ago improved treatment of common result name;
2001-11-11 ago added RAW_METHOD, RAW_METHOD_CASES;
2001-11-09 ago added impose_hyps_tac;
2001-11-05 ago pretty/print functions with context;
2001-10-31 ago 'atomize': CHANGED_PROP;
2001-10-27 ago declare equal_intr_rule as intro;
2001-10-27 ago added "atomize" method;
2001-10-23 ago trace_rules: only non-empty;
2001-10-16 ago proper order of kind names;
2001-10-15 ago intro! and elim! rules;
2001-10-14 ago atomize_tac etc. moved to object_logic.ML;
2001-10-12 ago added trace_rules, trace;
2001-01-16 ago added atomize_strip_tac;