src/Pure/Isar/proof.ML
2009-09-29 wenzelm 2009-09-29 explicit indication of Unsynchronized.ref;
2009-07-25 wenzelm 2009-07-25 basic method application: avoid Position.setmp_thread_data_seq, which destroys transaction context; Method.Basic: no position;
2009-07-25 wenzelm 2009-07-25 renamed structure Display_Goal to Goal_Display;
2009-07-24 wenzelm 2009-07-24 Display_Goal.pretty_goals: always Markup.subgoal, clarified options;
2009-07-23 wenzelm 2009-07-23 clarified pretty_goals, pretty_thm_aux: plain context; explicit pretty_goals_without_context, print_goals_without_context; tuned;
2009-07-21 wenzelm 2009-07-21 proper context for Display.pretty_thm etc. or old-style versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;
2009-07-20 wenzelm 2009-07-20 moved pretty_goals etc. to Display_Goal (required by tracing tacticals); load display.ML after assumption.ML, to accomodate proper contextual theorem display;
2009-07-20 wenzelm 2009-07-20 Proof.future_proof: declare all assumptions as well; Proof.future_proof: removed spurious exception_trace (which might cause crash-by-interrupt); replaced Future.fork_local by Future.fork_pri (again, until group exceptions are propagated properly);
2009-07-19 wenzelm 2009-07-19 parallel_proofs: more fine-grained control with optional parallel checking of nested Isar proofs;
2009-07-19 wenzelm 2009-07-19 more abstract Future.is_worker; Future.fork_local: inherit from worker (if available);
2009-03-28 wenzelm 2009-03-28 renamed ProofContext.add_fixes_i to ProofContext.add_fixes, eliminated obsolete external version;
2009-03-28 wenzelm 2009-03-28 renamed ProofContext.note_thmss_i to ProofContext.note_thmss, eliminated obsolete external version;
2009-03-28 wenzelm 2009-03-28 simplified references to facts, eliminated external note_thmss;
2009-03-28 wenzelm 2009-03-28 replaced add_binds(_i) by bind_terms -- internal version only;
2009-03-17 wenzelm 2009-03-17 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 wenzelm 2009-03-13 unified type Proof.method and pervasive METHOD combinators;
2009-03-10 wenzelm 2009-03-10 invoke_case: proper qualification of name binding, avoiding old no_base_names;
2009-03-05 wenzelm 2009-03-05 eliminated obsolete ProofContext.full_bname;
2009-03-03 wenzelm 2009-03-03 Thm.binding;
2009-01-21 haftmann 2009-01-21 binding is alias for Binding.T
2009-01-11 wenzelm 2009-01-11 added Goal.future_enabled abstraction -- now also checks that this is already a future task, which excludes interactive commands of the old toplevel;
2009-01-10 wenzelm 2009-01-10 added parallel_proofs flag (default true, cf. usedir option -Q), which can be disabled in low-memory situations;
2009-01-08 wenzelm 2009-01-08 tuned;
2009-01-08 haftmann 2009-01-08 made SML/NJ happy
2009-01-07 wenzelm 2009-01-07 future_proof: refined version covers local_future_proof and global_future_proof; future_proof: refrain from full Variable.auto_fixes -- not all contexts in the stack are in body mode; refined is_relevant: mode check; added local/global_future_terminal_proof;
2009-01-07 wenzelm 2009-01-07 qed/after_qed: singleton result;
2009-01-07 wenzelm 2009-01-07 future_terminal_proof: no fork for interactive mode, assert_backward;
2009-01-06 wenzelm 2009-01-06 future_terminal_proof: check Future.enabled;
2009-01-05 wenzelm 2009-01-05 added future_terminal_proof;
2009-01-04 wenzelm 2009-01-04 more precise is_relevant: requires original main goal, not initial goal state; tuned future_proof: minimal modification of goal state, retain original maxidx; tuned;
2008-12-12 wenzelm 2008-12-12 global_qed: refrain from ProofContext.auto_bind_facts, to avoid polluting the final result context with bindings involving loose free variables;
2008-12-05 wenzelm 2008-12-05 merged
2008-12-04 wenzelm 2008-12-04 future proofs: pass actual futures to facilitate composite computations;
2008-12-04 haftmann 2008-12-04 cleaned up binding module and related code
2008-10-16 wenzelm 2008-10-16 conclude_goal: precise goal context, include all sorts from context into statement, check shyps of result;
2008-10-02 wenzelm 2008-10-02 simplified Exn.EXCEPTIONS;
2008-10-01 wenzelm 2008-10-01 replaced can_defer by is_relevant (negation); future_proof: declare forked goal to prevent accidental generalization (e.g. instance goal);
2008-10-01 wenzelm 2008-10-01 future_proof: protect conclusion of deferred proof state;
2008-10-01 wenzelm 2008-10-01 renamed promise to future, tuned related interfaces;
2008-10-01 wenzelm 2008-10-01 more robust treatment of Interrupt (cf. exn.ML);
2008-09-30 wenzelm 2008-09-30 promise_proof: proper statement with empty vars;
2008-09-29 wenzelm 2008-09-29 promise global proofs;
2008-09-26 wenzelm 2008-09-26 eliminated polymorphic equality;
2008-09-18 wenzelm 2008-09-18 show: non-critical testing;
2008-09-17 wenzelm 2008-09-17 added map_contexts;
2008-09-02 wenzelm 2008-09-02 type Attrib.binding abbreviates Name.binding without attributes; Attrib.no_binding refers to Name.no_binding;
2008-09-02 wenzelm 2008-09-02 explicit type Name.binding for higher-specification elements;
2008-05-16 wenzelm 2008-05-16 removed obsolete case rule_context;
2008-03-19 wenzelm 2008-03-19 renamed datatype thmref to Facts.ref, tuned interfaces;
2008-03-11 wenzelm 2008-03-11 put_facts: do_props, i.e. facts are indexed by proposition again;
2008-01-24 wenzelm 2008-01-24 statement: keep explicit position; replaced ContextPosition by Position.thread_data;
2007-10-29 wenzelm 2007-10-29 test_proof: do not change Proofterm.proofs here (not thread-safe);
2007-10-11 wenzelm 2007-10-11 moved ProofContext.pp to Syntax.pp;
2007-10-09 wenzelm 2007-10-09 generic Syntax.pretty/string_of operations;
2007-10-01 wenzelm 2007-10-01 ContextPosition.put_ctxt;
2007-09-07 wenzelm 2007-09-07 reset goal messages after goal update;
2007-09-07 wenzelm 2007-09-07 made smlnj happy;
2007-09-06 wenzelm 2007-09-06 added goal_message;
2007-07-29 wenzelm 2007-07-29 renamed Drule.is_dummy_thm to Thm.is_dummy;
2007-07-27 wenzelm 2007-07-27 chain/using: filter out dummy_thm;