src/Pure/Isar/proof.ML
2013-04-03 wenzelm 2013-04-03 more explicit Goal.fork_params -- avoid implicit arguments via thread data; actually fork terminal proofs in interactive mode (amending 8707df0b0255);
2013-03-30 wenzelm 2013-03-30 more item markup; tuned signature;
2013-03-27 wenzelm 2013-03-27 more ambitious Goal.skip_proofs: covers Goal.prove forms as well, and do not insist in quick_and_dirty (for the sake of Isabelle/jEdit);
2013-03-27 wenzelm 2013-03-27 tuned signature and module arrangement;
2013-03-09 wenzelm 2013-03-09 tuned;
2013-03-04 wenzelm 2013-03-04 refined parallel_proofs = 2: fork whole Isar sub-proofs, not just terminal ones; refined parallel_proofs = 3: fork terminal proofs, as poor man's parallelization in interactive mode;
2013-02-28 wenzelm 2013-02-28 simplified Proof.future_proof;
2013-02-20 wenzelm 2013-02-20 proper check of Proof.is_relevant (again, cf. c3e99efacb67 and df8fc0567a3d);
2013-02-19 wenzelm 2013-02-19 improved scheduling of forked proofs, based on elapsed time estimate (from last run via session log file);
2013-01-25 wenzelm 2013-01-25 clarified notion of Command.proper_range (according to Token.is_proper), especially relevant for Active.try_replace_command, to avoid loosing subsequent comments accidentally; reverted f3588e59aeaa accordingly;
2013-01-16 wenzelm 2013-01-16 proper range position;
2013-01-14 wenzelm 2013-01-14 restrict "bad" markup to command keyword, notably excluding subsequent comments;
2012-12-03 wenzelm 2012-12-03 recovered error to finish proof (e.g. bad obtain export) from 223f18cfbb32; tuned message;
2012-11-25 wenzelm 2012-11-25 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
2012-10-18 wenzelm 2012-10-18 more robust future_proof result with specific error message (e.g. relevant for incomplete proof of non-registered theorem);
2012-10-18 wenzelm 2012-10-18 tuned message;
2012-10-18 wenzelm 2012-10-18 avoid spurious "bad" markup for show/test_proof; tuned;
2012-10-17 wenzelm 2012-10-17 skipped proofs appear as "bad" without counting as error;
2012-10-17 wenzelm 2012-10-17 more method position information, notably finished_pos after end of previous text;
2012-10-16 wenzelm 2012-10-16 tuned messages;
2012-10-16 wenzelm 2012-10-16 more proof method text position information;
2012-10-16 wenzelm 2012-10-16 clarified defer/prefer: more specific errors;
2012-10-16 wenzelm 2012-10-16 more informative errors for 'proof' and 'apply' steps; more Seq.result operations;
2012-10-16 wenzelm 2012-10-16 more informative error for stand-alone 'qed';
2012-10-16 wenzelm 2012-10-16 further attempts to unify/simplify goal output;
2012-10-16 wenzelm 2012-10-16 more informative error messages of initial/terminal proof methods; more systematic support for sequences with embedded errors; tuned Seq.maps;
2012-10-13 wenzelm 2012-10-13 more informative error of initial/terminal proof steps;
2012-10-13 wenzelm 2012-10-13 some attempts to unify/simplify pretty_goal;
2012-10-13 wenzelm 2012-10-13 refined Proof.the_finished_goal with more informative error; more permissive Method.all_assm_tac: do not insist in solving by assumption here to postpone failure; clarified Method.finish_text: no Thm.no_prems filtering here to postpone failure;
2012-10-09 wenzelm 2012-10-09 clarified Local_Defs.add_def(s): refrain from hard-wiring Thm.def_binding_optional; clarified Generic_Target.define: avoid duplicate def binding via Local_Defs.add_def;
2012-09-01 wenzelm 2012-09-01 removed unused material;
2012-09-01 wenzelm 2012-09-01 discontinued complicated/unreliable notion of recent proofs within context;
2012-08-31 wenzelm 2012-08-31 more precise register_proofs for local goals; tuned signature;
2012-08-30 wenzelm 2012-08-30 register proofs of Isar goals, to enable recovery from unstable command states after interactive cancellation;
2012-08-30 wenzelm 2012-08-30 refined treatment of forked proofs at transaction boundaries, including proof commands (see also 7ee000ce5390); stretched meaning of Goal.parallel_proofs to enable future_terminal_proofs in interactive document model, despite its lack for regular forking of proofs;
2012-08-30 wenzelm 2012-08-30 some support for registering forked proofs within Proof.state, using its bottom context; tuned signature;
2012-04-27 wenzelm 2012-04-27 clarified signature;
2012-04-12 wenzelm 2012-04-12 more precise declaration of goal_tfrees in forked proof state;
2012-04-10 wenzelm 2012-04-10 static relevance of proof via syntax keywords;
2012-03-21 wenzelm 2012-03-21 tuned signature;
2012-03-21 wenzelm 2012-03-21 tuned messages;
2012-03-21 wenzelm 2012-03-21 prefer explicitly qualified exception List.Empty;
2012-03-18 wenzelm 2012-03-18 maintain generic context naming in structure Name_Space (NB: empty = default_naming, init = local_naming); more explicit Context.generic for Name_Space.declare/define and derivatives (NB: naming changed after Proof_Context.init_global); prefer Context.pretty in low-level operations of structure Sorts/Type (defer full Syntax.init_pretty until error output); simplified signatures;
2012-02-28 wenzelm 2012-02-28 display proof results as "state", to suppress odd squiggles in the Prover IDE (see also 9240be8c8c69);
2012-02-14 wenzelm 2012-02-14 tuned signature, according to actual usage of these operations;
2011-11-28 wenzelm 2011-11-28 separate module for concrete Isabelle markup;
2011-11-20 wenzelm 2011-11-20 uniform cert_vars/read_vars;
2011-11-07 wenzelm 2011-11-07 tuned signature -- avoid spurious Thm.mixed_attribute;
2011-11-03 wenzelm 2011-11-03 tuned signature -- canonical argument order;
2011-08-01 nipkow 2011-08-01 infrastructure for attaching names to hypothesis in cases; realised via the same tag mechanism as case names
2011-07-11 wenzelm 2011-07-11 tuned signature -- corresponding to Scala version;
2011-05-12 wenzelm 2011-05-12 proper configuration options Proof_Context.debug and Proof_Context.verbose; discontinued alias Proof.verbose = Proof_Context.verbose;
2011-04-27 wenzelm 2011-04-27 more precise positions via binding;
2011-04-16 wenzelm 2011-04-16 modernized structure Proof_Context;
2011-04-08 wenzelm 2011-04-08 discontinued special treatment of structure Mixfix; eliminated slightly odd no_syn convenience;
2011-03-21 wenzelm 2011-03-21 tuned;
2011-01-31 wenzelm 2011-01-31 more specific Goal.fork_name;
2010-12-15 wenzelm 2010-12-15 show: display goal refinement rule as "state", to avoid odd Output.urgent_message and make its association with the goal more explicit;
2010-12-04 wenzelm 2010-12-04 formal notepad without any result;
2010-11-22 bulwahn 2010-11-22 added useful function map_context_result to signature