src/Pure/Isar/proof.ML
2006-11-28 wenzelm 2006-11-28 simplified '?' operator;
2006-11-22 wenzelm 2006-11-22 init: enter inner statement mode, which prevents local notes from being named internally;
2006-11-21 wenzelm 2006-11-21 made SML/NJ happy;
2006-11-21 wenzelm 2006-11-21 removed obsolete simple_note_thms;
2006-11-21 wenzelm 2006-11-21 simplified theorem(_i); notes: proper kind; renamed put_thms_internal to put_thms;
2006-11-14 wenzelm 2006-11-14 simplified Proof.theorem(_i) interface -- removed target support; removed obsolete global_goal interface; removed goal_names, simplified goal kind output; tuned;
2006-11-09 wenzelm 2006-11-09 Stack.map_top;
2006-10-09 wenzelm 2006-10-09 def(_i): LocalDefs.add_defs; removed Drule.strip_shyps_warning;
2006-10-07 wenzelm 2006-10-07 tuned;
2006-08-09 wenzelm 2006-08-09 global goals/qeds: after_qed operates on Proof.context (potentially local_theory);
2006-08-05 wenzelm 2006-08-05 removed obsolete sign_of;
2006-08-02 wenzelm 2006-08-02 simplified Assumption/ProofContext.export; simplified end_block;
2006-07-27 wenzelm 2006-07-27 moved basic assumption operations from structure ProofContext to Assumption;
2006-07-26 wenzelm 2006-07-26 export goal_tac (was internal refine_tac);
2006-07-06 wenzelm 2006-07-06 apply_text: support Method.Source_i;
2006-07-04 wenzelm 2006-07-04 added schematic_goal;
2006-06-17 wenzelm 2006-06-17 ProofContext.exports: simultaneous facts; Variable.exportT_terms;
2006-06-15 wenzelm 2006-06-15 ProofContext: moved variable operations to struct Variable; tuned;
2006-06-12 wenzelm 2006-06-12 Unify.matches_list;
2006-06-11 wenzelm 2006-06-11 fixes: include mixfix syntax; goal: improved handling of implicit vars;
2006-06-05 wenzelm 2006-06-05 allow non-trivial schematic goals (via embedded term vars);
2006-05-07 wenzelm 2006-05-07 removed 'concl is' patterns;
2006-04-27 wenzelm 2006-04-27 tuned basic list operators (flat, maps, map_filter);
2006-04-26 wenzelm 2006-04-26 curried Seq.cons;
2006-04-13 wenzelm 2006-04-13 use conjunction stuff from conjunction.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;