src/Pure/Isar/proof.ML
2001-10-13 wenzelm 2001-10-13 generic theorem kinds;
2001-09-08 wenzelm 2001-09-08 print_state: subgoals;
2001-09-04 wenzelm 2001-09-04 renamed "antecedent" case to "rule_context";
2001-08-31 berghofe 2001-08-31 Tuned naming of theorems.
2001-02-07 wenzelm 2001-02-07 val get_goal: state -> context * (thm list * thm);
2001-01-18 wenzelm 2001-01-18 made SML/XL happy;
2001-01-18 wenzelm 2001-01-18 show(_i): check goal;
2001-01-09 wenzelm 2001-01-09 avoid renaming of params in cases;
2001-01-06 wenzelm 2001-01-06 moved norm_hhf_tac to Pure/tactic.ML; adapted invoke_case;
2000-11-30 wenzelm 2000-11-30 removed get_goal; suffer schematic (top-level) goals;
2000-11-21 wenzelm 2000-11-21 tag result with name reference to final binding (basically just a comment);
2000-11-13 wenzelm 2000-11-13 tuned statement args;
2000-11-10 wenzelm 2000-11-10 norm_hhf_tac;
2000-11-06 wenzelm 2000-11-06 RuleCases.make true;
2000-11-03 wenzelm 2000-11-03 tuned names;
2000-10-30 wenzelm 2000-10-30 tuned goals output;
2000-10-30 nipkow 2000-10-30 Added antiquotation "subgoals".
2000-10-24 wenzelm 2000-10-24 added pretty_goals;
2000-08-01 wenzelm 2000-08-01 tuned;
2000-07-30 wenzelm 2000-07-30 export RANGE, hard_asm_tac, soft_asm_tac; export is_chain, assert_forward_or_chain; added the_fact; updated ProofContext.export_wrt;
2000-07-13 wenzelm 2000-07-13 invoke_case: bind_skolem;
2000-06-29 wenzelm 2000-06-29 facts: handle multiple lists of arguments;
2000-05-28 wenzelm 2000-05-28 case 'antecedent';
2000-05-05 wenzelm 2000-05-05 GPLed;
2000-04-17 wenzelm 2000-04-17 tuned msg;
2000-04-15 wenzelm 2000-04-15 next_block: reset_facts;
2000-04-05 wenzelm 2000-04-05 tuned comment;
2000-03-30 wenzelm 2000-03-30 support Hindley-Milner polymorphisms in binds and facts; let_bind(_i): polymorphic version; moved find_free, export_wrt to Isar/proof_context.ML;
2000-03-26 wenzelm 2000-03-26 tuned output;
2000-03-23 wenzelm 2000-03-23 tuned output;
2000-03-21 wenzelm 2000-03-21 soft_asm_tac: hack to norm goal;
2000-03-17 wenzelm 2000-03-17 next_block: allow in non-goal blocks as well (experimental);
2000-03-15 wenzelm 2000-03-15 pretty chunks;
2000-03-14 wenzelm 2000-03-14 invoke_case: include attributes;
2000-03-08 wenzelm 2000-03-08 invoke_case: name assumption;
2000-03-08 wenzelm 2000-03-08 generalized FINDGOAL, HEADGOAL; handling of local contexts: method_cases, invoke_case;
2000-02-14 wenzelm 2000-02-14 tuned msg;
2000-02-13 wenzelm 2000-02-13 refine_end;
2000-02-07 wenzelm 2000-02-07 assert_no_chain;
2000-02-02 wenzelm 2000-02-02 most_general_varify_tfrees all results;
2000-01-28 wenzelm 2000-01-28 added HEADGOAL;
2000-01-28 wenzelm 2000-01-28 replaced FIRSTGOAL by FINDGOAL (backtracking!); improved flexflex handling; tuned sig;
2000-01-05 wenzelm 2000-01-05 tuned;
1999-10-25 wenzelm 1999-10-25 improved handling of warn_extra_tfrees;
1999-10-22 wenzelm 1999-10-22 warn_extra_tfrees; removed bind(_i), add_binds, declare_term;
1999-09-30 wenzelm 1999-09-30 export find_free;
1999-09-30 wenzelm 1999-09-30 get_goal: prop; fix_i: typ option;
1999-09-29 wenzelm 1999-09-29 removed extra shyps error;
1999-09-25 wenzelm 1999-09-25 added reset_thms; prep_result: check prop;
1999-09-22 wenzelm 1999-09-22 tuned pretty_thms;
1999-09-22 wenzelm 1999-09-22 improved output;
1999-09-21 wenzelm 1999-09-21 setup_goal: do not insert assumptions;
1999-09-06 wenzelm 1999-09-06 close_block: removed ProofContext.transfer_used_names;
1999-09-04 wenzelm 1999-09-04 deactivated ProofContext.transfer_used_names; eliminated PureThy.default_name ("" not stored);
1999-09-01 wenzelm 1999-09-01 removed the_fact; added pretty_thms; fix: common constraints; renamed "facts" to "this"; print_state: tuned "Using facts";
1999-08-18 wenzelm 1999-08-18 assume: multiple args;
1999-08-09 wenzelm 1999-08-09 tuned print_state;
1999-08-05 wenzelm 1999-08-05 local goals: after_qed;
1999-07-15 wenzelm 1999-07-15 export init_state; end_proof: reset goal_facts;
1999-07-13 wenzelm 1999-07-13 handle cgoal;