src/Pure/Isar/proof_context.ML
1999-09-25 wenzelm 1999-09-25 added reset_thms; add_binds(_i): admit unbinding;
1999-09-22 wenzelm 1999-09-22 improved output;
1999-09-21 wenzelm 1999-09-21 export prems_of;
1999-09-07 wenzelm 1999-09-07 read_def_termT: dummyT;
1999-09-06 wenzelm 1999-09-06 removed thms_closure (unused); removed transfer_used_names; fix: do not declare unconstrained vars;
1999-09-04 wenzelm 1999-09-04 eliminated Syntax.binding; put_thms: ignore ""; update_binds_env: Envir.norm_term ensures proper type instantiation;
1999-09-01 wenzelm 1999-09-01 fix: common constraints;
1999-08-18 wenzelm 1999-08-18 warn_vars; tuned strings_of_context; assume(_i): multiple args;
1999-08-09 wenzelm 1999-08-09 tuned strings_of_context; fix: check identifier;
1999-07-13 wenzelm 1999-07-13 handle cgoal;
1999-07-12 wenzelm 1999-07-12 added show_hyps flag;
1999-07-08 wenzelm 1999-07-08 propp: 'concl' patterns; assumptions: tactics for non-goal export; use Display.pretty_thm_no_hyps;
1999-07-04 wenzelm 1999-07-04 added transfer_used_names;
1999-07-01 wenzelm 1999-07-01 have_thmss: more_ths;
1999-07-01 wenzelm 1999-07-01 setmp Display.show_hyps false;
1999-06-28 wenzelm 1999-06-28 tuned;
1999-06-28 wenzelm 1999-06-28 tuned output: print_context replaced by strings_of_context; assumptions: back-pressure solver as parameter;
1999-06-07 wenzelm 1999-06-07 improved handling of assumptions;
1999-06-05 wenzelm 1999-06-05 auto_bind_goal, auto_bind_facts;
1999-06-02 wenzelm 1999-06-02 read_term/prop_pat: do not freeze;
1999-05-24 wenzelm 1999-05-24 tuned print_context;
1999-05-01 wenzelm 1999-05-01 renamed 'dummy' to 'dummy_pattern' (less dangerous);
1999-04-30 wenzelm 1999-04-30 dummy patterns; theory data: copy;
1999-04-27 wenzelm 1999-04-27 verbose flag;
1999-01-12 wenzelm 1999-01-12 eliminated tthm type and Attribute structure;
1998-11-29 wenzelm 1998-11-29 fixed declatation of patterns and skolem;
1998-11-19 wenzelm 1998-11-19 term_pat vs. prop_pat; added bind_propp(_i); assume: propp;
1998-11-17 wenzelm 1998-11-17 have_tthms; assume: store actual asms;
1998-11-16 wenzelm 1998-11-16 renamed init_context to init; added read_termTs; added declare_thm;
1998-11-09 wenzelm 1998-11-09 Proof context information.