src/Pure/Isar/proof.ML
2006-03-21 wenzelm 2006-03-21 avoid polymorphic equality; subtract (op =);
2006-03-08 wenzelm 2006-03-08 select_goals: split original conjunctions;
2006-03-04 wenzelm 2006-03-04 method: SelectGoals;
2006-02-17 wenzelm 2006-02-17 global_qeds: transfer body context;
2006-02-16 wenzelm 2006-02-16 added put_thms_internal; tuned;
2006-02-10 wenzelm 2006-02-10 tuned comment;
2006-02-02 wenzelm 2006-02-02 added refine_insert;
2006-01-31 wenzelm 2006-01-31 tuned LocalDefs.unfold;
2006-01-29 wenzelm 2006-01-29 'unfolding': LocalDefs.unfold;
2006-01-28 wenzelm 2006-01-28 LocalDefs; unfolding(_i): support object-level rewrites;
2006-01-27 wenzelm 2006-01-27 swapped Toplevel.theory_context; tuned;
2006-01-25 wenzelm 2006-01-25 ProofContext.export_standard;
2006-01-21 wenzelm 2006-01-21 simplified type attribute;
2006-01-14 wenzelm 2006-01-14 sane ERROR handling;
2006-01-13 wenzelm 2006-01-13 uniform handling of fixes;
2006-01-07 wenzelm 2006-01-07 RuleCases.make_common;
2006-01-03 wenzelm 2006-01-03 added unfolding(_i); renamed using_thmss(_i) to using_i;
2005-12-23 wenzelm 2005-12-23 goal/qed: proper treatment of two levels of conjunctions;
2005-12-22 wenzelm 2005-12-22 auto cases: marked improper; tuned;
2005-12-21 haftmann 2005-12-21 discontinued unflat in favour of burrow and burrow_split
2005-12-09 haftmann 2005-12-09 oriented result pairs in PureThy
2005-11-30 wenzelm 2005-11-30 simulaneous 'def';
2005-11-22 wenzelm 2005-11-22 cases_tactic;
2005-11-16 wenzelm 2005-11-16 ProofContext.mk_def;
2005-11-08 wenzelm 2005-11-08 simplified after_qed;
2005-10-28 wenzelm 2005-10-28 renamed Goal constant to prop, more general protect/unprotect interfaces; tuned ProofContext.export interfaces;
2005-10-21 wenzelm 2005-10-21 export add_binds_i; invoke_case: AutoBind.no_facts; Goal.init, Goal.conclude;
2005-10-18 wenzelm 2005-10-18 tuned error msg;
2005-10-15 wenzelm 2005-10-15 goal statements: before_qed argument;
2005-10-04 wenzelm 2005-10-04 minor tweaks for Poplog/ML;
2005-09-17 wenzelm 2005-09-17 export put_facts; moved auto_fix to proof_context.ML; generic_goal: solve 0 subgoals initially; global_goal/theorem: only store results if SOME target, which may be empty;
2005-09-16 ballarin 2005-09-16 interpretation uses primitive goal interface
2005-09-13 wenzelm 2005-09-13 major cleanup of interfaces and implementation; generic goal commands: local/global_goal with after_qed; independent of locale.ML; more self-contained proof elements (material from isar_thy.ML); refer to ProofDisplay (cf. proof_display.ML); unified print_results (always normal); added get_thmss;
2005-08-31 wenzelm 2005-08-31 refer to theory instead of low-level tsig;
2005-08-28 wenzelm 2005-08-28 tuned;
2005-08-18 wenzelm 2005-08-18 moved after method.ML; moved FINDGOAL/HEADGOAL to method.ML; moved type method to method.ML; prepare attributes here; tuned various interfaces (cf. isar_thy.ML); tuned;
2005-08-08 ballarin 2005-08-08 After_qed takes result argument.
2005-07-13 wenzelm 2005-07-13 removed ad-hoc atp_hook, cal_atp; removed depth_of; tuned;
2005-06-22 wenzelm 2005-06-22 added depth_of;
2005-06-17 wenzelm 2005-06-17 RuleCases.tactic; accomodate identification of type Sign.sg and theory;
2005-06-01 ballarin 2005-06-01 Locales: new element constrains, parameter renaming with syntax, experimental command instantiate withdrawn.
2005-05-31 wenzelm 2005-05-31 method_cases: RuleCases.T option; goal cases: remove previous ones; invoke_case: ProofContext.no_base_names o ProofContext.qualified_names; undefined rule_context: remove instead of empty one; tuned;
2005-05-17 wenzelm 2005-05-17 tuned;
2005-05-17 wenzelm 2005-05-17 tuned;
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.