src/Pure/Isar/proof.ML
2000-04-05 ago tuned comment;
2000-03-30 ago support Hindley-Milner polymorphisms in binds and facts;
2000-03-26 ago tuned output;
2000-03-23 ago tuned output;
2000-03-21 ago soft_asm_tac: hack to norm goal;
2000-03-17 ago next_block: allow in non-goal blocks as well (experimental);
2000-03-15 ago pretty chunks;
2000-03-14 ago invoke_case: include attributes;
2000-03-08 ago invoke_case: name assumption;
2000-03-08 ago generalized FINDGOAL, HEADGOAL;
2000-02-14 ago tuned msg;
2000-02-13 ago refine_end;
2000-02-07 ago assert_no_chain;
2000-02-02 ago most_general_varify_tfrees all results;
2000-01-28 ago added HEADGOAL;
2000-01-28 ago replaced FIRSTGOAL by FINDGOAL (backtracking!);
2000-01-05 ago tuned;
1999-10-25 ago improved handling of warn_extra_tfrees;
1999-10-22 ago warn_extra_tfrees;
1999-09-30 ago export find_free;
1999-09-30 ago get_goal: prop;
1999-09-29 ago removed extra shyps error;
1999-09-25 ago added reset_thms;
1999-09-22 ago tuned pretty_thms;
1999-09-22 ago improved output;
1999-09-21 ago setup_goal: do not insert assumptions;
1999-09-06 ago close_block: removed ProofContext.transfer_used_names;
1999-09-04 ago deactivated ProofContext.transfer_used_names;
1999-09-01 ago removed the_fact;
1999-08-18 ago assume: multiple args;
1999-08-09 ago tuned print_state;
1999-08-05 ago local goals: after_qed;
1999-07-15 ago export init_state;
1999-07-13 ago handle cgoal;
1999-07-12 ago added show_hyps flag;
1999-07-09 ago global_qed: removed alt_name, alt_att;
1999-07-08 ago propp: 'concl' patterns;
1999-07-04 ago close_block: transfer_used_names;
1999-07-03 ago tuned print_state;
1999-07-02 ago generalized fixes get index 0;
1999-07-01 ago have_thmss: more_ths;
1999-07-01 ago added check_result;
1999-06-28 ago improved RANGE;
1999-06-28 ago tuned print_state;
1999-06-07 ago tuned mode_name;
1999-06-05 ago auto_bind_goal, auto_bind_facts;
1999-06-04 ago added the_fact, level;
1999-06-01 ago improved print_state;
1999-05-31 ago setup_goal: proper handling of non-atomic goals (include cprems into asms);
1999-05-26 ago cleaned comments;
1999-05-21 ago local_qed: obtain interactive flag;
1999-04-27 ago improved print_state;
1999-03-19 ago common qed and end of proofs;
1999-02-08 ago tuned msg;
1999-01-12 ago eliminated tthm type and Attribute structure;
1998-12-17 ago tuned mode_name;
1998-12-01 ago qed: kind_name (again);
1998-11-29 ago tuned print_state;
1998-11-21 ago print_state: use begin_goal from Goals.current_goals_markers;
1998-11-19 ago match_bind(_i): 'as' patterns;