src/Pure/Isar/method.ML
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;
2000-03-08 wenzelm 2000-03-08 added METHOD_CASES, resolveq_cases_tac; removed multi_resolveq; improved 'tactic' method: bind thm(s) function;
2000-03-06 wenzelm 2000-03-06 added simple_args; added 'tactic' method;
2000-03-03 wenzelm 2000-03-03 added multi_resolveq, resolveq_tac;
2000-03-02 wenzelm 2000-03-02 added 'prolog' method;
2000-02-22 wenzelm 2000-02-22 tuned syntax wrapper;
2000-02-14 wenzelm 2000-02-14 proof step: reset goal_facts;
2000-02-14 wenzelm 2000-02-14 fixed prefer;
2000-02-13 wenzelm 2000-02-13 added refine_end; res_inst tactic emulation;
2000-02-09 wenzelm 2000-02-09 [df]rule methods;
2000-02-07 wenzelm 2000-02-07 refine_no_facts: recover goal_facts;
2000-02-05 wenzelm 2000-02-05 '.' == by this;
2000-01-28 wenzelm 2000-01-28 added prefer, defer;
2000-01-28 wenzelm 2000-01-28 maintain standard rules (beware: classical provers provides another version!);
2000-01-05 wenzelm 2000-01-05 added thms_ctxt_args;
1999-09-30 wenzelm 1999-09-30 insert: ignore facts;
1999-09-26 wenzelm 1999-09-26 help: unkown theory context;
1999-09-25 wenzelm 1999-09-25 simplified sectioned_args; tuned;
1999-09-22 wenzelm 1999-09-22 added 'insert' method (again);
1999-09-21 wenzelm 1999-09-21 setup for refined facts handling; tuned insert_facts, assumption, (un)fold; insert_tac: no rotate_tac, order was OK in the first place; added ctxt_args, bang_sectioned_args; added assm_tac;
1999-09-08 wenzelm 1999-09-08 (un)fold: ignore facts;
1999-09-07 wenzelm 1999-09-07 Method.refine_no_facts;
1999-09-07 wenzelm 1999-09-07 then_tac = refine;
1999-09-02 wenzelm 1999-09-02 terminal method: always involve finish;
1999-09-01 wenzelm 1999-09-01 tuned; renamed same_tac to insert_tac; improved assumption; removed Repeat; immediate_proof: assumption;
1999-08-26 wenzelm 1999-08-26 print_help;
1999-08-18 wenzelm 1999-08-18 sectioned_args etc.: more general modifier;
1999-07-30 wenzelm 1999-07-30 added erule; renamed same to -;
1999-07-12 wenzelm 1999-07-12 export assumption_tac; local qeds: print rule; same_tac: actually insert rules, !! bind vars;
1999-07-09 wenzelm 1999-07-09 global_qed: removed alt_name, alt_att;
1999-07-08 wenzelm 1999-07-08 terminal_proof: 2nd method;
1999-07-01 wenzelm 1999-07-01 fixed backtracking of global_qed;
1999-06-28 wenzelm 1999-06-28 cond_extern_table; datatype method = Method of thm list -> tactic;