src/Pure/Isar/method.ML
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;
1999-06-04 wenzelm 1999-06-04 export multi_resolve;
1999-05-26 wenzelm 1999-05-26 local_qed: print_result;
1999-05-21 wenzelm 1999-05-21 local_qed: obtain interactive flag;
1999-04-30 wenzelm 1999-04-30 theory data: copy;
1999-04-27 wenzelm 1999-04-27 fold / unfold methods;
1999-04-23 wenzelm 1999-04-23 added FINISHED, same_tac;
1999-03-19 wenzelm 1999-03-19 common qed and end of proofs;
1999-01-12 wenzelm 1999-01-12 'same' method, 'immediate' proof;
1999-01-12 wenzelm 1999-01-12 improved asm_finish;
1999-01-12 wenzelm 1999-01-12 eliminated tthm type and Attribute structure;
1998-11-18 wenzelm 1998-11-18 removed trace;
1998-11-17 wenzelm 1998-11-17 exception METHOD_FAIL;
1998-11-16 wenzelm 1998-11-16 several args parsers; realistic syntax; tuned;
1998-11-09 wenzelm 1998-11-09 Proof methods.