src/Pure/Isar/proof.ML
2004-06-21 kleing 2004-06-21 Merged in license change from Isabelle2004
2004-06-05 wenzelm 2004-06-05 pretty_thm/goals_aux, pretty_flexpair: pp;
2004-04-14 wenzelm 2004-04-14 renamed have_thms to note_thms;
2004-04-13 wenzelm 2004-04-13 export put_thms; do not export use_facts, reset_facts;
2004-04-13 kleing 2004-04-13 export thisN
2004-04-07 ballarin 2004-04-07 Locale instantiation: label parameter optional, new attribute paramter.
2004-04-02 ballarin 2004-04-02 Experimental command for instantiation of locales in proof contexts: instantiate <label>: <loc>
2004-02-21 nipkow 2004-02-21 Transitive_Closure: added consumes and case_names attributes Isar: fixed parameter name handling in simulatneous induction which I had not done properly 2 years ago.
2003-09-30 ballarin 2003-09-30 Improvements to Isar/Locales: premises generated by "includes" elements changed. Bugfix "unify_frozen".
2003-07-24 berghofe 2003-07-24 Exported function get_mode.
2003-03-18 nipkow 2003-03-18 toggled show_main_goal
2002-11-07 nipkow 2002-11-07 added show_main_goal
2002-09-30 nipkow 2002-09-30 modified induct method
2002-07-26 wenzelm 2002-07-26 support for split assumptions in cases (hyps vs. prems);
2002-07-24 wenzelm 2002-07-24 tuned view;
2002-07-19 wenzelm 2002-07-19 support locale ``views'' (for cumulative predicates);
2002-07-16 wenzelm 2002-07-16 export map_context; removed internal interface put_data;
2002-07-10 wenzelm 2002-07-10 tuned Locale.add_thmss;
2002-07-04 wenzelm 2002-07-04 tuned;
2002-07-02 wenzelm 2002-07-02 these_facts: refrain from put_thmss (2nd time!);
2002-02-27 wenzelm 2002-02-27 tuned feedback of goal forms;
2002-02-26 wenzelm 2002-02-26 clarified localized multi statements;
2002-02-24 wenzelm 2002-02-24 added using_thmss(_i);
2002-01-17 wenzelm 2002-01-17 RuleCases.make interface based on term instead of thm; tuned;
2002-01-15 wenzelm 2002-01-15 allow zero goals;
2002-01-11 wenzelm 2002-01-11 have_thmss vs. have_thmss_i; with_thmss vs. with_thmss_i;
2002-01-10 wenzelm 2002-01-10 refine_tac: Tactic.norm_hhf_tac before trying rule; global_qed: uses Locale.add_thmss_hybrid, tuned;
2002-01-10 wenzelm 2002-01-10 locales: hide base name of exported version;
2001-12-19 wenzelm 2001-12-19 tuned interface of ProofContext.generalize; tuned;
2001-12-18 wenzelm 2001-12-18 use Locale.read/cert_context_statement;
2001-12-14 wenzelm 2001-12-14 tuned locale interface;
2001-12-14 wenzelm 2001-12-14 Locale.activate_context;
2001-12-08 wenzelm 2001-12-08 tuned print_state interfaces;
2001-11-28 wenzelm 2001-11-28 print_state: up to 7 result names;
2001-11-19 wenzelm 2001-11-19 improved treatment of common result name;
2001-11-19 wenzelm 2001-11-19 multi_theorem: common statement header (covers *all* results);
2001-11-16 wenzelm 2001-11-16 finish_global: Drule.strip_shyps_warning (just for warning);
2001-11-12 wenzelm 2001-11-12 empty rule_context for multiple goals;
2001-11-11 wenzelm 2001-11-11 added multi_theorem(_i); have, show etc.: multiple statements;
2001-11-07 wenzelm 2001-11-07 locale_prefix: Sign.base_name;
2001-11-06 wenzelm 2001-11-06 pretty_goals_local: observes context syntax; PureThy.store_thm: locale_prefix;
2001-11-06 wenzelm 2001-11-06 theorem(_i): locale atts; global_goal, finish_global: proper treatment of target locale;
2001-11-05 wenzelm 2001-11-05 pretty/print functions with context;
2001-11-04 wenzelm 2001-11-04 theorem(_i): locale elements;
2001-11-01 wenzelm 2001-11-01 theorem: locale argument;
2001-10-31 wenzelm 2001-10-31 theorem(_i): locale argument; contexts 0 and 1 in state now refer to theory and locale, respectively; unified export (no longer uses global "standard");
2001-10-31 berghofe 2001-10-31 Removed name_thm from finish_global.
2001-10-31 wenzelm 2001-10-31 finish_global: Tactic.norm_hhf;
2001-10-30 wenzelm 2001-10-30 tuned;
2001-10-24 wenzelm 2001-10-24 simplified ProofContext.assume interface;
2001-10-23 wenzelm 2001-10-23 moved RANGE to tctical.ML; moved export_assume, export_presume, export_def to proof_context.ML;
2001-10-23 wenzelm 2001-10-23 removed export_thm;
2001-10-22 wenzelm 2001-10-22 moved local defs to proof.ML (for locales);
2001-10-16 wenzelm 2001-10-16 simplified exporter interface;
2001-10-16 wenzelm 2001-10-16 support impromptu terminology of cases parameters;
2001-10-13 wenzelm 2001-10-13 generic theorem kinds;
2001-09-08 wenzelm 2001-09-08 print_state: subgoals;
2001-09-04 wenzelm 2001-09-04 renamed "antecedent" case to "rule_context";
2001-08-31 berghofe 2001-08-31 Tuned naming of theorems.
2001-02-07 wenzelm 2001-02-07 val get_goal: state -> context * (thm list * thm);