isabelle: Graph

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
tuned imports;
2013-03-26, by wenzelm
tuned proofs;
2013-03-26, by wenzelm
explicit sublocale dependency for Min/Max yields more appropriate Min/Max prefix for a couple of facts
2013-03-26, by haftmann
merged
2013-03-26, by wenzelm
proper input event handling;
2013-03-26, by wenzelm
more standard imports;
2013-03-26, by wenzelm
more specific Entry painting;
2013-03-26, by wenzelm
tuned;
2013-03-26, by wenzelm
mixed theory/command entries;
2013-03-26, by wenzelm
dockable window for timing information;
2013-03-26, by wenzelm
no \FIXME macro for ProgProve (moved to book)
2013-03-26, by kleing
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
2013-03-26, by hoelzl
rename eventually_at / _within, to distinguish them from the lemmas in the HOL image
2013-03-26, by hoelzl
move theorems about compactness of real closed intervals, the intermediate value theorem, and lemmas about continuity of bijective functions from Deriv.thy to Limits.thy
2013-03-26, by hoelzl
Series.thy is based on Limits.thy and not Deriv.thy
2013-03-26, by hoelzl
move Ln.thy and Log.thy to Transcendental.thy
2013-03-26, by hoelzl
move SEQ.thy and Lim.thy to Limits.thy
2013-03-26, by hoelzl
HOL-NSA should only import Complex_Main
2013-03-26, by hoelzl
rename RealVector.thy to Real_Vector_Spaces.thy
2013-03-26, by hoelzl
rename RealDef to Real
2013-03-26, by hoelzl
remove Real.thy
2013-03-26, by hoelzl
merge RComplete into RealDef
2013-03-26, by hoelzl
move real_isLub_unique to isLub_unique in Lubs; real_sum_of_halves to RealDef; abs_diff_less_iff to Rings
2013-03-26, by hoelzl
remove posreal_complete
2013-03-26, by hoelzl
separate SupInf into Conditional_Complete_Lattice, move instantiation of real to RealDef
2013-03-26, by hoelzl
Discontinued theories src/HOL/Algebra/abstract and .../poly.
2013-03-25, by ballarin
Remove obsolete URLs in documentation of HOL-Algebra.
2013-03-25, by ballarin
Fix issue related to mixins in roundup.
2013-03-25, by ballarin