src/Pure/Isar/method.ML
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;
2001-12-03 wenzelm 2001-12-03 added "rules" method;
2001-11-29 wenzelm 2001-11-29 rule context and attributes moved to rule_context.ML;
2001-11-28 wenzelm 2001-11-28 theory data: removed obsolete finish method;
2001-11-21 wenzelm 2001-11-21 use tracing function for trace output;
2001-11-19 wenzelm 2001-11-19 improved treatment of common result name;
2001-11-11 wenzelm 2001-11-11 added RAW_METHOD, RAW_METHOD_CASES; METHOD, METHOD_CASES etc.: conjunction_tac;
2001-11-09 wenzelm 2001-11-09 added impose_hyps_tac; robustify insts of tactic emulations;
2001-11-05 wenzelm 2001-11-05 pretty/print functions with context;
2001-10-31 wenzelm 2001-10-31 'atomize': CHANGED_PROP;
2001-10-27 wenzelm 2001-10-27 declare equal_intr_rule as intro;
2001-10-27 wenzelm 2001-10-27 added "atomize" method;
2001-10-23 wenzelm 2001-10-23 trace_rules: only non-empty;
2001-10-16 wenzelm 2001-10-16 proper order of kind names;
2001-10-15 wenzelm 2001-10-15 intro! and elim! rules;
2001-10-14 wenzelm 2001-10-14 atomize_tac etc. moved to object_logic.ML;
2001-10-12 wenzelm 2001-10-12 added trace_rules, trace;
2001-01-16 wenzelm 2001-01-16 added atomize_strip_tac;
2001-01-07 wenzelm 2001-01-07 CHANGED_PROP;
2000-12-27 wenzelm 2000-12-27 'erule' etc.: assm arg;
2000-11-29 wenzelm 2000-11-29 resolveq(_cases)_tac moved to HOL/Tools/induct_method.ML;
2000-11-28 wenzelm 2000-11-28 resolveq_cases_tac: insert facts;
2000-11-10 wenzelm 2000-11-10 rewrite_goal_tac moved to tactic.ML;
2000-11-07 berghofe 2000-11-07 Moved rewriting functions from Thm to MetaSimplifier.
2000-11-06 wenzelm 2000-11-06 added rewrite_goal_tac; resolveq_cases_tac: generalized args; tuned atomize; assm_tac: include reflexive_thm;
2000-11-03 wenzelm 2000-11-03 assumption / finish: handle non-atomic assumptions from context as well;
2000-10-23 wenzelm 2000-10-23 intro_classes by default;
2000-09-19 wenzelm 2000-09-19 tuned args;
2000-09-17 wenzelm 2000-09-17 Display.pretty_thm_sg;
2000-09-13 wenzelm 2000-09-13 Args.addN, Args.delN;
2000-09-12 wenzelm 2000-09-12 delrule: handle dest rules as well; replaced "delrule" by "rule del";
2000-09-07 wenzelm 2000-09-07 tuned msgs;
2000-09-05 wenzelm 2000-09-05 generalized types of args;
2000-09-01 wenzelm 2000-09-01 added bang_sectioned_args';
2000-08-28 wenzelm 2000-08-28 removed METHOD0; added SIMPLE_METHOD('); added thm_args;
2000-08-18 wenzelm 2000-08-18 fixed RuleCases.make (invert flag);
2000-08-17 wenzelm 2000-08-17 cases: opaque by default; fixed ML tactic: proper context; added 'rename_tac', 'rename_tac';
2000-08-14 wenzelm 2000-08-14 tuned msg;
2000-08-09 wenzelm 2000-08-09 res_inst: include non-inst versions with multiple thms; ML tactic: thms closure; tuned msgs;
2000-08-04 wenzelm 2000-08-04 added goal_args('); added "cut_tac", "thin_tac", "rename_tac"; renamed inst tactics; inst syntax: include empty inst;
2000-08-01 wenzelm 2000-08-01 added atomize_goal / atomize_tac;
2000-08-01 wenzelm 2000-08-01 (un)fold: CHANGED; added atomize_tac;
2000-07-24 wenzelm 2000-07-24 Drule.merge_rules;
2000-07-13 wenzelm 2000-07-13 RuleCases.make opaq;
2000-07-01 wenzelm 2000-07-01 removed help_methods; tuned print_methods;
2000-06-29 wenzelm 2000-06-29 added add_method;
2000-05-24 wenzelm 2000-05-24 added "done" proof;
2000-05-05 wenzelm 2000-05-05 GPLed;
2000-04-17 wenzelm 2000-04-17 Pretty.chunks;
2000-04-05 wenzelm 2000-04-05 HEADGOAL;
2000-03-30 wenzelm 2000-03-30 'tactic': refer to PureIsar structure;
2000-03-20 wenzelm 2000-03-20 use Args.goal_spec; added subgoal_tac;
2000-03-18 wenzelm 2000-03-18 tuned comments;
2000-03-08 wenzelm 2000-03-08 sect: exlude ":" from parser;