src/Pure/Isar/proof.ML
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.