2013-04-09 ago wenzelm just one timing protocol function, with 3 implementations: TTY/PG, PIDE/document, build;
2013-04-09 ago wenzelm clarified protocol_message undefinedness;
2013-04-09 ago wenzelm quote by Alan Kay;
2013-04-09 ago wenzelm more accurate documentation;
2013-04-09 ago wenzelm discontinued Toplevel.no_timing complication -- also recovers timing of diagnostic commands, e.g. 'find_theorems';
2013-04-09 ago wenzelm more accurate documentation of "(structure)" mixfix;
2013-04-09 ago wenzelm more robust static structure reference, avoid dynamic Proof_Context.intern_skolem in Syntax_Phases.decode_term;
2013-04-09 ago wenzelm tuned comment;
2013-04-09 ago wenzelm just one syntax category "mixfix" -- check structure annotation semantically;
2013-04-09 ago wenzelm tuned message;
2013-04-09 ago blanchet handle case clashes on Mac file system by encoding goal numbers
2013-04-09 ago blanchet avoid duplicate "tcon_" names
2013-04-09 ago blanchet smoothly handle cyclic graphs
2013-04-09 ago blanchet compile + fixed naming convention
2013-04-09 ago blanchet reverted accidental changes to theory file + updated wrt ML file
2013-04-09 ago blanchet no need to filter tautologies anymore -- they are prefiltered by "all_facts"'
2013-04-09 ago blanchet work on CASC LTB ISA exporter
2013-04-09 ago blanchet tuning
2013-04-09 ago hoelzl add continuous_on rules for products
2013-04-09 ago hoelzl fixed spelling
2013-04-09 ago hoelzl move FrechetDeriv from the Library to HOL/Deriv; base DERIV on FDERIV and both derivatives allow a restricted support set; FDERIV is now an abbreviation of has_derivative
2013-04-09 ago hoelzl remove the within-filter, replace "at" by "at _ within UNIV" (This allows to remove a couple of redundant lemmas)
2013-04-08 ago wenzelm improved printing of exception CTERM (see also d0f0f37ec346);
2013-04-08 ago wenzelm prefer pretty_exn where possible -- NB: low-level General.exnMessage may still be used elsewhere (e.g. by the ML compiler itself);
2013-04-08 ago wenzelm more defensive representation of forced break within PolyML.PrettyBreak -- avoid accidental blowup if low-level operations are used, notably PolyML.makestring or its variant General.exnMessage;
2013-04-08 ago wenzelm discontinued odd magic number, which was once used for performance measurements;
2013-04-08 ago wenzelm document @{make_string}, cf. NEWS of Isabelle2009-2 (June 2010);
2013-04-08 ago wenzelm merged
2013-04-08 ago wenzelm more general Thy_Load.import_name, e.g. relevant for Isabelle/eclipse -- NB: Thy_Load serves as main hub for funny overriding to adapt to provers and editors;
2013-04-08 ago blanchet try to preserve original linearization
2013-04-08 ago blanchet use somewhat lighter encoding
2013-04-08 ago blanchet robustness w.r.t. unknown arguments
2013-04-07 ago nipkow cleaned
2013-04-07 ago nipkow cleaned
2013-04-06 ago nipkow tuned
2013-04-05 ago wenzelm tuned signature -- agree with markup terminology;
2013-04-05 ago wenzelm unified terminology with Markup.DOCUMENT_SOURCE in Scala, which is unused but displayed as "document source" entity in Isabelle/jEdit;
2013-04-05 ago nipkow tuned document
2013-04-05 ago nipkow tuned
2013-04-04 ago haftmann sup on multisets
2013-04-04 ago haftmann convenient induction rule
2013-04-04 ago wenzelm tuned README -- less buzzwords;
2013-04-04 ago wenzelm more conventional synchronized access to Options_Variable -- avoid Swing_Thread getting in the way, which might be absent in some environments (e.g. SWT);
2013-04-04 ago wenzelm added missing file;
2013-04-04 ago wenzelm tuned signature -- avoid intrusion of slightly odd Swing structures into pure Markup_Tree;
2013-04-04 ago wenzelm tuned signature -- concentrate GUI tools;
2013-04-04 ago wenzelm tuned signature -- concentrate GUI tools;
2013-04-04 ago wenzelm separate module "GUI", to keep this out of the way of generic Isabelle_System operations, notably for non-Isabelle/jEdit applications;
2013-04-04 ago wenzelm separate module Isabelle_Font, to keep this out of the way of generic Isabelle_System operations, notably for non-Isabelle/jEdit applications;
2013-04-04 ago wenzelm tuned imports;
2013-04-04 ago wenzelm added var_position in analogy to longid_position, for typing reports on input;
2013-04-04 ago nipkow removed unnerving (esp in jedit) and pointless warning
2013-04-04 ago nipkow tuned
2013-04-03 ago wenzelm merged
2013-04-03 ago wenzelm tuned;
2013-04-03 ago wenzelm recover implicit thread position for status messages (cf. eca8acb42e4a);
2013-04-03 ago wenzelm additional timing status for implicitly forked terminal proofs -- proper accounting for interactive Timing dockable etc.;
2013-04-03 ago wenzelm more explicit Goal.fork_params -- avoid implicit arguments via thread data;
2013-04-03 ago wenzelm updated comment to 46b90bbc370d;
2013-04-03 ago wenzelm recovered proper transaction position for Goal.fork error reporting (lost in 8e9746e584c9);