src/Pure/Isar/proof.ML
2005-04-17 wenzelm 2005-04-17 tuned comments;
2005-04-13 wenzelm 2005-04-13 *** MESSAGE REFERS TO PREVIOUS VERSION *** Attrib.src; removed Locale.multi_attribute (pass Attrib.src instead); removed interpret(_i) (use have_i instead); goals: more uniform treatment of after_qed, removed separate thy_mod of global goals;
2005-04-13 wenzelm 2005-04-13 *** empty log message ***
2005-04-11 ballarin 2005-04-11 First release of interpretation commands.
2005-03-24 ballarin 2005-03-24 Further work on interpretation commands. New command `interpret' for interpretation in proof contexts.
2005-03-09 ballarin 2005-03-09 First version of global registration command.
2005-03-04 skalberg 2005-03-04 Removed practically all references to Library.foldr.
2005-03-03 skalberg 2005-03-03 Move towards standard functions.
2005-02-15 berghofe 2005-02-15 refine now provides specific cases "goal1" ... "goaln" for addressing subgoals of a proof state.
2005-02-13 skalberg 2005-02-13 Deleted Library.option type.
2005-01-24 berghofe 2005-01-24 Specific theorems in a named list of theorems can now be referred to via indices (type thmref).
2005-01-21 paulson 2005-01-21 Jia Meng: delta simpsets and clasets
2004-09-28 ballarin 2004-09-28 Bug fixes.
2004-09-27 ballarin 2004-09-27 Modified locales: improved implementation of "includes".
2004-09-09 paulson 2004-09-09 new hooks for resolution by Jia Meng
2004-08-12 ballarin 2004-08-12 Disallowed "includes" in locale declarations.
2004-08-02 ballarin 2004-08-02 Some comments added.
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;