src/Pure/Isar/proof.ML
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;
1999-07-12 wenzelm 1999-07-12 added show_hyps flag; local qed: print rule;
1999-07-09 wenzelm 1999-07-09 global_qed: removed alt_name, alt_att; setup_goal: proper order of prems;
1999-07-08 wenzelm 1999-07-08 propp: 'concl' patterns; assumptions: tactics for non-goal export; use Display.pretty_thm_no_hyps; assm vs. assume vs. presume; tuned type goal; tuned print_goal; relative exports, absolute export_thm rule; transfer_facts; tuned;
1999-07-04 wenzelm 1999-07-04 close_block: transfer_used_names; tuned;
1999-07-03 wenzelm 1999-07-03 tuned print_state;
1999-07-02 wenzelm 1999-07-02 generalized fixes get index 0;
1999-07-01 wenzelm 1999-07-01 have_thmss: more_ths; simple_have_thmss;
1999-07-01 wenzelm 1999-07-01 added check_result; setmp Display.show_hyps false; fixed auto_bind_facts; tuned finish_proof; fixed backtracking of global_qed;
1999-06-28 wenzelm 1999-06-28 improved RANGE;
1999-06-28 wenzelm 1999-06-28 tuned print_state; datatype method = Method of thm list -> tactic; assumptions: back-pressure solver as parameter;
1999-06-07 wenzelm 1999-06-07 tuned mode_name; improved handling of assumptions; eliminated let_thms (named prop bindings moved to auto_bind.ML);
1999-06-05 wenzelm 1999-06-05 auto_bind_goal, auto_bind_facts; varify_tfrees: no longer generalize types of free term variables; let_thms: no bindings;
1999-06-04 wenzelm 1999-06-04 added the_fact, level;
1999-06-01 wenzelm 1999-06-01 improved print_state;
1999-05-31 wenzelm 1999-05-31 setup_goal: proper handling of non-atomic goals (include cprems into asms);
1999-05-26 wenzelm 1999-05-26 cleaned comments; local_qed: print_result argument; prep_result: always varify type variables (Thm.varifyT);
1999-05-21 wenzelm 1999-05-21 local_qed: obtain interactive flag;
1999-04-27 wenzelm 1999-04-27 improved print_state;
1999-03-19 wenzelm 1999-03-19 common qed and end of proofs;
1999-02-08 wenzelm 1999-02-08 tuned msg;
1999-01-12 wenzelm 1999-01-12 eliminated tthm type and Attribute structure;
1998-12-17 wenzelm 1998-12-17 tuned mode_name;
1998-12-01 wenzelm 1998-12-01 qed: kind_name (again);
1998-11-29 wenzelm 1998-11-29 tuned print_state; changed solve semantics: support back-pressure of asms (cut, def etc.);
1998-11-21 wenzelm 1998-11-21 print_state: use begin_goal from Goals.current_goals_markers;
1998-11-19 wenzelm 1998-11-19 match_bind(_i): 'as' patterns; assume, theorem, show etc.: propp; tuned qed msg;
1998-11-17 wenzelm 1998-11-17 PureThy.default_name; have_tthms;
1998-11-16 wenzelm 1998-11-16 renamed init_context to init;
1998-11-09 wenzelm 1998-11-09 Proof states and methods.