src/Pure/Isar/proof.ML
2010-05-29 ago explicit markup for forked goals, as indicated by Goal.fork;
2010-04-29 ago 'write': actually observe the proof structure (like 'let' or 'fix');
2010-04-29 ago ProofContext.read_const: allow for type constraint (for fixed variable);
2010-04-26 ago eliminanated some unreferenced identifiers;
2010-04-25 ago removed obsolete/unused Proof.match_bind;
2010-04-25 ago modernized naming conventions of main Isar proof elements;
2010-04-25 ago goals: simplified handling of implicit variables -- removed obsolete warning;
2010-03-07 ago modernized structure Local_Defs;
2010-01-15 ago Eliminated is_open option of Rule_Cases.make_nested/make_common;
2010-01-04 ago after_qed: refrain from Position.setmp_thread_data, which causes duplication of results with several independent proof attempts;
2009-11-02 ago modernized structure Proof_Display;
2009-11-02 ago modernized structure AutoBind;
2009-11-01 ago modernized structure Rule_Cases;
2009-10-28 ago replaced slightly odd get_goal/flat_goal by explicit goal views that correspond to the usual method categories;
2009-10-25 ago more direct access to naming;
2009-10-20 ago backpatching of structure Proof and ProofContext -- avoid odd aliases;
2009-10-02 ago clarified Proof.refine_insert -- always "refine" to apply standard method treatment (of conjunctions);
2009-09-30 ago eliminated dead code;
2009-09-30 ago replaced chained_goal by slightly more appropriate flat_goal;
2009-09-30 ago added chained_goal, which presents the goal thm as seen by semi-structured methods;
2009-09-29 ago explicit indication of Unsynchronized.ref;
2009-07-25 ago basic method application: avoid Position.setmp_thread_data_seq, which destroys transaction context;
2009-07-25 ago renamed structure Display_Goal to Goal_Display;
2009-07-24 ago Display_Goal.pretty_goals: always Markup.subgoal, clarified options;
2009-07-23 ago clarified pretty_goals, pretty_thm_aux: plain context;
2009-07-21 ago proper context for Display.pretty_thm etc. or old-style versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;
2009-07-20 ago moved pretty_goals etc. to Display_Goal (required by tracing tacticals);
2009-07-20 ago Proof.future_proof: declare all assumptions as well;
2009-07-19 ago parallel_proofs: more fine-grained control with optional parallel checking of nested Isar proofs;
2009-07-19 ago more abstract Future.is_worker;
2009-03-28 ago renamed ProofContext.add_fixes_i to ProofContext.add_fixes, eliminated obsolete external version;
2009-03-28 ago renamed ProofContext.note_thmss_i to ProofContext.note_thmss, eliminated obsolete external version;
2009-03-28 ago simplified references to facts, eliminated external note_thmss;
2009-03-28 ago replaced add_binds(_i) by bind_terms -- internal version only;
2009-03-17 ago goal_tac: finish marked assumptions from left to right -- corresponds better with the strategy of etac, with significant performance gains in some situations;
2009-03-13 ago unified type Proof.method and pervasive METHOD combinators;
2009-03-10 ago invoke_case: proper qualification of name binding, avoiding old no_base_names;
2009-03-05 ago eliminated obsolete ProofContext.full_bname;
2009-03-03 ago Thm.binding;
2009-01-21 ago binding is alias for Binding.T
2009-01-11 ago added Goal.future_enabled abstraction -- now also checks that this is already
2009-01-10 ago added parallel_proofs flag (default true, cf. usedir option -Q), which can be disabled in low-memory situations;
2009-01-08 ago tuned;
2009-01-08 ago made SML/NJ happy
2009-01-07 ago future_proof: refined version covers local_future_proof and global_future_proof;
2009-01-07 ago qed/after_qed: singleton result;
2009-01-07 ago future_terminal_proof: no fork for interactive mode, assert_backward;
2009-01-06 ago future_terminal_proof: check Future.enabled;
2009-01-05 ago added future_terminal_proof;
2009-01-04 ago more precise is_relevant: requires original main goal, not initial goal state;
2008-12-12 ago global_qed: refrain from ProofContext.auto_bind_facts, to avoid
2008-12-05 ago merged
2008-12-04 ago future proofs: pass actual futures to facilitate composite computations;
2008-12-04 ago cleaned up binding module and related code
2008-10-16 ago conclude_goal: precise goal context, include all sorts from context into statement, check shyps of result;
2008-10-02 ago simplified Exn.EXCEPTIONS;
2008-10-01 ago replaced can_defer by is_relevant (negation);
2008-10-01 ago future_proof: protect conclusion of deferred proof state;
2008-10-01 ago renamed promise to future, tuned related interfaces;
2008-10-01 ago more robust treatment of Interrupt (cf. exn.ML);