src/Pure/Isar/proof.ML
2013-04-09 ago just one timing protocol function, with 3 implementations: TTY/PG, PIDE/document, build;
2013-04-03 ago additional timing status for implicitly forked terminal proofs -- proper accounting for interactive Timing dockable etc.;
2013-04-03 ago more explicit Goal.fork_params -- avoid implicit arguments via thread data;
2013-03-30 ago more item markup;
2013-03-27 ago 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 ago tuned signature and module arrangement;
2013-03-09 ago tuned;
2013-03-04 ago refined parallel_proofs = 2: fork whole Isar sub-proofs, not just terminal ones;
2013-02-28 ago simplified Proof.future_proof;
2013-02-20 ago proper check of Proof.is_relevant (again, cf. c3e99efacb67 and df8fc0567a3d);
2013-02-19 ago improved scheduling of forked proofs, based on elapsed time estimate (from last run via session log file);
2013-01-25 ago clarified notion of Command.proper_range (according to Token.is_proper), especially relevant for Active.try_replace_command, to avoid loosing subsequent comments accidentally;
2013-01-16 ago proper range position;
2013-01-14 ago restrict "bad" markup to command keyword, notably excluding subsequent comments;
2012-12-03 ago recovered error to finish proof (e.g. bad obtain export) from 223f18cfbb32;
2012-11-25 ago Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
2012-10-18 ago more robust future_proof result with specific error message (e.g. relevant for incomplete proof of non-registered theorem);
2012-10-18 ago tuned message;
2012-10-18 ago avoid spurious "bad" markup for show/test_proof;
2012-10-17 ago skipped proofs appear as "bad" without counting as error;
2012-10-17 ago more method position information, notably finished_pos after end of previous text;
2012-10-16 ago tuned messages;
2012-10-16 ago more proof method text position information;
2012-10-16 ago clarified defer/prefer: more specific errors;
2012-10-16 ago more informative errors for 'proof' and 'apply' steps;
2012-10-16 ago more informative error for stand-alone 'qed';
2012-10-16 ago further attempts to unify/simplify goal output;
2012-10-16 ago more informative error messages of initial/terminal proof methods;
2012-10-13 ago more informative error of initial/terminal proof steps;
2012-10-13 ago some attempts to unify/simplify pretty_goal;
2012-10-13 ago refined Proof.the_finished_goal with more informative error;
2012-10-09 ago clarified Local_Defs.add_def(s): refrain from hard-wiring Thm.def_binding_optional;
2012-09-01 ago removed unused material;
2012-09-01 ago discontinued complicated/unreliable notion of recent proofs within context;
2012-08-31 ago more precise register_proofs for local goals;
2012-08-30 ago register proofs of Isar goals, to enable recovery from unstable command states after interactive cancellation;
2012-08-30 ago refined treatment of forked proofs at transaction boundaries, including proof commands (see also 7ee000ce5390);
2012-08-30 ago some support for registering forked proofs within Proof.state, using its bottom context;
2012-04-27 ago clarified signature;
2012-04-12 ago more precise declaration of goal_tfrees in forked proof state;
2012-04-10 ago static relevance of proof via syntax keywords;
2012-03-21 ago tuned signature;
2012-03-21 ago tuned messages;
2012-03-21 ago prefer explicitly qualified exception List.Empty;
2012-03-18 ago maintain generic context naming in structure Name_Space (NB: empty = default_naming, init = local_naming);
2012-02-28 ago display proof results as "state", to suppress odd squiggles in the Prover IDE (see also 9240be8c8c69);
2012-02-14 ago tuned signature, according to actual usage of these operations;
2011-11-28 ago separate module for concrete Isabelle markup;
2011-11-20 ago uniform cert_vars/read_vars;
2011-11-07 ago tuned signature -- avoid spurious Thm.mixed_attribute;
2011-11-03 ago tuned signature -- canonical argument order;
2011-08-01 ago infrastructure for attaching names to hypothesis in cases; realised via the same tag mechanism as case names
2011-07-11 ago tuned signature -- corresponding to Scala version;
2011-05-12 ago proper configuration options Proof_Context.debug and Proof_Context.verbose;
2011-04-27 ago more precise positions via binding;
2011-04-16 ago modernized structure Proof_Context;
2011-04-08 ago discontinued special treatment of structure Mixfix;
2011-03-21 ago tuned;
2011-01-31 ago more specific Goal.fork_name;
2010-12-15 ago show: display goal refinement rule as "state", to avoid odd Output.urgent_message and make its association with the goal more explicit;