isabelle: Graph

Mercurial Mercurial > repos > isabelle / graph

summary | shortlog | changelog | graph | tags | bookmarks | branches | files | gz | help
less more | (0) -30000 -10000 -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 +30000 tip

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

less more | (0) -30000 -10000 -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 +30000 tip

isabelle