src/Pure/Isar/proof.ML
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;
1998-11-17 ago PureThy.default_name;
1998-11-16 ago renamed init_context to init;
1998-11-09 ago Proof states and methods.