src/Pure/Isar/proof.ML
2005-03-24 ago Further work on interpretation commands. New command `interpret' for
2005-03-09 ago First version of global registration command.
2005-03-04 ago Removed practically all references to Library.foldr.
2005-03-03 ago Move towards standard functions.
2005-02-15 ago refine now provides specific cases "goal1" ... "goaln" for addressing
2005-02-13 ago Deleted Library.option type.
2005-01-24 ago Specific theorems in a named list of theorems can now be referred to
2005-01-21 ago Jia Meng: delta simpsets and clasets
2004-09-28 ago Bug fixes.
2004-09-27 ago Modified locales: improved implementation of "includes".
2004-09-09 ago new hooks for resolution by Jia Meng
2004-08-12 ago Disallowed "includes" in locale declarations.
2004-08-02 ago Some comments added.
2004-06-21 ago Merged in license change from Isabelle2004
2004-06-05 ago pretty_thm/goals_aux, pretty_flexpair: pp;
2004-04-14 ago renamed have_thms to note_thms;
2004-04-13 ago export put_thms;
2004-04-13 ago export thisN
2004-04-07 ago Locale instantiation: label parameter optional, new attribute paramter.
2004-04-02 ago Experimental command for instantiation of locales in proof contexts:
2004-02-21 ago Transitive_Closure: added consumes and case_names attributes
2003-09-30 ago Improvements to Isar/Locales: premises generated by "includes" elements
2003-07-24 ago Exported function get_mode.
2003-03-18 ago toggled show_main_goal
2002-11-07 ago added show_main_goal
2002-09-30 ago modified induct method
2002-07-26 ago support for split assumptions in cases (hyps vs. prems);
2002-07-24 ago tuned view;
2002-07-19 ago support locale ``views'' (for cumulative predicates);
2002-07-16 ago export map_context;
2002-07-10 ago tuned Locale.add_thmss;
2002-07-04 ago tuned;
2002-07-02 ago these_facts: refrain from put_thmss (2nd time!);
2002-02-27 ago tuned feedback of goal forms;
2002-02-26 ago clarified localized multi statements;
2002-02-24 ago added using_thmss(_i);
2002-01-17 ago RuleCases.make interface based on term instead of thm;
2002-01-15 ago allow zero goals;
2002-01-11 ago have_thmss vs. have_thmss_i;
2002-01-10 ago refine_tac: Tactic.norm_hhf_tac before trying rule;
2002-01-10 ago locales: hide base name of exported version;
2001-12-19 ago tuned interface of ProofContext.generalize;
2001-12-18 ago use Locale.read/cert_context_statement;
2001-12-14 ago tuned locale interface;
2001-12-14 ago Locale.activate_context;
2001-12-08 ago tuned print_state interfaces;
2001-11-28 ago print_state: up to 7 result names;
2001-11-19 ago improved treatment of common result name;
2001-11-19 ago multi_theorem: common statement header (covers *all* results);
2001-11-16 ago finish_global: Drule.strip_shyps_warning (just for warning);
2001-11-12 ago empty rule_context for multiple goals;
2001-11-11 ago added multi_theorem(_i);
2001-11-07 ago locale_prefix: Sign.base_name;
2001-11-06 ago pretty_goals_local: observes context syntax;
2001-11-06 ago theorem(_i): locale atts;
2001-11-05 ago pretty/print functions with context;
2001-11-04 ago theorem(_i): locale elements;
2001-11-01 ago theorem: locale argument;
2001-10-31 ago theorem(_i): locale argument;
2001-10-31 ago Removed name_thm from finish_global.