src/Pure/Isar/method.ML
2000-04-05 ago HEADGOAL;
2000-03-30 ago 'tactic': refer to PureIsar structure;
2000-03-20 ago use Args.goal_spec;
2000-03-18 ago tuned comments;
2000-03-08 ago sect: exlude ":" from parser;
2000-03-08 ago added METHOD_CASES, resolveq_cases_tac;
2000-03-06 ago added simple_args;
2000-03-03 ago added multi_resolveq, resolveq_tac;
2000-03-02 ago added 'prolog' method;
2000-02-22 ago tuned syntax wrapper;
2000-02-14 ago proof step: reset goal_facts;
2000-02-14 ago fixed prefer;
2000-02-13 ago added refine_end;
2000-02-09 ago [df]rule methods;
2000-02-07 ago refine_no_facts: recover goal_facts;
2000-02-05 ago '.' == by this;
2000-01-28 ago added prefer, defer;
2000-01-28 ago maintain standard rules (beware: classical provers provides another version!);
2000-01-05 ago added thms_ctxt_args;
1999-09-30 ago insert: ignore facts;
1999-09-26 ago help: unkown theory context;
1999-09-25 ago simplified sectioned_args;
1999-09-22 ago added 'insert' method (again);
1999-09-21 ago setup for refined facts handling;
1999-09-08 ago (un)fold: ignore facts;
1999-09-07 ago Method.refine_no_facts;
1999-09-07 ago then_tac = refine;
1999-09-02 ago terminal method: always involve finish;
1999-09-01 ago tuned;
1999-08-26 ago print_help;
1999-08-18 ago sectioned_args etc.: more general modifier;
1999-07-30 ago added erule;
1999-07-12 ago export assumption_tac;
1999-07-09 ago global_qed: removed alt_name, alt_att;
1999-07-08 ago terminal_proof: 2nd method;
1999-07-01 ago fixed backtracking of global_qed;
1999-06-28 ago cond_extern_table;
1999-06-04 ago export multi_resolve;
1999-05-26 ago local_qed: print_result;
1999-05-21 ago local_qed: obtain interactive flag;
1999-04-30 ago theory data: copy;
1999-04-27 ago fold / unfold methods;
1999-04-23 ago added FINISHED, same_tac;
1999-03-19 ago common qed and end of proofs;
1999-01-12 ago 'same' method, 'immediate' proof;
1999-01-12 ago improved asm_finish;
1999-01-12 ago eliminated tthm type and Attribute structure;
1998-11-18 ago removed trace;
1998-11-17 ago exception METHOD_FAIL;
1998-11-16 ago several args parsers;
1998-11-09 ago Proof methods.