isabelle: Graph

just one timing protocol function, with 3 implementations: TTY/PG, PIDE/document, build;
2013-04-09, by wenzelm
clarified protocol_message undefinedness;
2013-04-09, by wenzelm
quote by Alan Kay;
2013-04-09, by wenzelm
more accurate documentation;
2013-04-09, by wenzelm
discontinued Toplevel.no_timing complication -- also recovers timing of diagnostic commands, e.g. 'find_theorems';
2013-04-09, by wenzelm
more accurate documentation of "(structure)" mixfix;
2013-04-09, by wenzelm
more robust static structure reference, avoid dynamic Proof_Context.intern_skolem in Syntax_Phases.decode_term;
2013-04-09, by wenzelm
tuned comment;
2013-04-09, by wenzelm
just one syntax category "mixfix" -- check structure annotation semantically;
2013-04-09, by wenzelm
tuned message;
2013-04-09, by wenzelm
handle case clashes on Mac file system by encoding goal numbers
2013-04-09, by blanchet
avoid duplicate "tcon_" names
2013-04-09, by blanchet
smoothly handle cyclic graphs
2013-04-09, by blanchet
compile + fixed naming convention
2013-04-09, by blanchet
reverted accidental changes to theory file + updated wrt ML file
2013-04-09, by blanchet
no need to filter tautologies anymore -- they are prefiltered by "all_facts"'
2013-04-09, by blanchet
work on CASC LTB ISA exporter
2013-04-09, by blanchet
tuning
2013-04-09, by blanchet
add continuous_on rules for products
2013-04-09, by hoelzl
fixed spelling
2013-04-09, by 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, by hoelzl
remove the within-filter, replace "at" by "at _ within UNIV" (This allows to remove a couple of redundant lemmas)
2013-04-09, by hoelzl
improved printing of exception CTERM (see also d0f0f37ec346);
2013-04-08, by 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, by 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, by wenzelm
discontinued odd magic number, which was once used for performance measurements;
2013-04-08, by wenzelm
document @{make_string}, cf. NEWS of Isabelle2009-2 (June 2010);
2013-04-08, by wenzelm
merged
2013-04-08, by 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, by wenzelm
try to preserve original linearization
2013-04-08, by blanchet
use somewhat lighter encoding
2013-04-08, by blanchet
robustness w.r.t. unknown arguments
2013-04-08, by blanchet
cleaned
2013-04-07, by nipkow
cleaned
2013-04-07, by nipkow
tuned
2013-04-06, by nipkow
tuned signature -- agree with markup terminology;
2013-04-05, by wenzelm
unified terminology with Markup.DOCUMENT_SOURCE in Scala, which is unused but displayed as "document source" entity in Isabelle/jEdit;
2013-04-05, by wenzelm
tuned document
2013-04-05, by nipkow
tuned
2013-04-05, by nipkow
sup on multisets
2013-04-04, by haftmann
convenient induction rule
2013-04-04, by haftmann
tuned README -- less buzzwords;
2013-04-04, by 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, by wenzelm
added missing file;
2013-04-04, by wenzelm
tuned signature -- avoid intrusion of slightly odd Swing structures into pure Markup_Tree;
2013-04-04, by wenzelm
tuned signature -- concentrate GUI tools;
2013-04-04, by wenzelm
tuned signature -- concentrate GUI tools;
2013-04-04, by 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, by 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, by wenzelm
tuned imports;
2013-04-04, by wenzelm
added var_position in analogy to longid_position, for typing reports on input;
2013-04-04, by wenzelm
removed unnerving (esp in jedit) and pointless warning
2013-04-04, by nipkow
tuned
2013-04-04, by nipkow
merged
2013-04-03, by wenzelm
tuned;
2013-04-03, by wenzelm
recover implicit thread position for status messages (cf. eca8acb42e4a);
2013-04-03, by wenzelm
additional timing status for implicitly forked terminal proofs -- proper accounting for interactive Timing dockable etc.;
2013-04-03, by wenzelm
more explicit Goal.fork_params -- avoid implicit arguments via thread data;
2013-04-03, by wenzelm
updated comment to 46b90bbc370d;
2013-04-03, by wenzelm
recovered proper transaction position for Goal.fork error reporting (lost in 8e9746e584c9);
2013-04-03, by wenzelm
tuned -- Drule.comp_no_flatten includes Drule.incr_indexes already (NB: result should be deterministic by construction);
2013-04-03, by wenzelm
tuned output -- less bullets;
2013-04-03, by wenzelm
default implementation of multisets by list with reasonable coverage of operations on multisets
2013-04-03, by haftmann
optionalized very specific code setup for multisets
2013-04-03, by haftmann
generalized lemma fold_image thanks to Peter Lammich
2013-04-03, by haftmann
tuned;
2013-04-02, by wenzelm
NEWS for 635562bc14ef;
2013-04-02, by wenzelm
more centralized command timing;
2013-04-02, by wenzelm
got rid of legacy smartness
2013-04-02, by blanchet
added lemma
2013-04-01, by nipkow
merged
2013-03-30, by wenzelm
amended uncond_skel to observe notion of cong_name properly -- may affect simplification with Free congs;
2013-03-30, by wenzelm
more formal cong_name;
2013-03-30, by wenzelm
timing status for forked diagnostic commands;
2013-03-30, by wenzelm
tooltip of command keyword includes timing information;
2013-03-30, by wenzelm
more operations on Time, Timing;
2013-03-30, by wenzelm
reverted slip introduced in f738e6dbd844
2013-03-29, by haftmann
added 'print_defn_rules' command;
2013-03-30, by wenzelm
more item markup;
2013-03-30, by wenzelm
item markup for Proof_Context.pretty_fact;
2013-03-30, by wenzelm
obsolete, cf. Proof_Context.print_syntax;
2013-03-30, by wenzelm
paint bullet bar within text layer -- thus it remains visible with active selection etc.;
2013-03-29, by wenzelm
Pretty.item markup for improved readability of lists of items;
2013-03-29, by wenzelm
tuned message;
2013-03-29, by wenzelm
convenience check for vain instantiation
2013-03-29, by haftmann
improved centering via strikethrough offset;
2013-03-29, by wenzelm
re-generated SMT certificates
2013-03-28, by boehmes
new, simpler implementation of monomorphization;
2013-03-28, by boehmes
ghost bullet via markup, which is painted as bar under text (normally space);
2013-03-28, by wenzelm
replace induction by hammer
2013-03-28, by kleing
merged
2013-03-28, by wenzelm
merged;
2013-03-28, by wenzelm
basic support for Pretty.item, which is considered as logical markup and interpreted in Isabelle/Scala, but ignored elsewhere (TTY, latex etc.);
2013-03-28, by wenzelm
maintain integer indentation during formatting -- it needs to be implemented by repeated spaces eventually;
2013-03-28, by wenzelm
tuned;
2013-03-28, by wenzelm
proper default browser info for interactive mode, notably thy_deps;
2013-03-28, by wenzelm
improved pretty printing for state set acom
2013-03-28, by nipkow
Improvements to the print_dependencies command.
2013-03-27, by ballarin
discontinued obsolete parallel_proofs_reuse_timing;
2013-03-27, by wenzelm
merged
2013-03-27, by wenzelm
separate isatest with skip_proofs, to give some impression of performance without most of the proofs;
2013-03-27, by wenzelm
merged
2013-03-27, by wenzelm
extra checkpoint to avoid stale theory in skip_proof context, e.g. in 'instance' proof;
2013-03-27, by wenzelm
tuned;
2013-03-27, by wenzelm
allow build with skip_proofs enabled -- disable it for sessions that would fail due to embedded diagnostic commands, for example;
2013-03-27, by wenzelm
more robust access Toplevel.proof_of -- prefer warning via Toplevel.unknown_proof over hard crash (notably for skipped proofs);
2013-03-27, by wenzelm
more liberal handling of skipped proofs;
2013-03-27, by wenzelm
explicit Toplevel.is_skipped_proof;
2013-03-27, by wenzelm
separate option editor_skip_proofs, to avoid accidental change of preferences for skip_proofs, which would invalidate batch builds;
2013-03-27, by wenzelm
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, by wenzelm
clarified Skip_Proof.cheat_tac: more standard tactic;
2013-03-27, by wenzelm
tuned signature and module arrangement;
2013-03-27, by wenzelm
tuned;
2013-03-27, by wenzelm
tuned GUI;
2013-03-27, by wenzelm
centralized various multiset operations in theory multiset;
2013-03-27, by haftmann
avoid odd foundational terms after interpretation;
2013-03-26, by haftmann
more uniform style for interpretation and sublocale declarations
2013-03-26, by haftmann
merged
2013-03-26, by wenzelm
tuned session specification;
2013-03-26, by wenzelm
tuned proof;
2013-03-26, by wenzelm