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