2013-07-03 wenzelm 2013-07-03 allow multiple print functions;
2013-07-03 wenzelm 2013-07-03 tuned signature;
2013-07-03 wenzelm 2013-07-03 tuned signature;
2013-07-03 wenzelm 2013-07-03 tuned;
2013-07-03 wenzelm 2013-07-03 tuned signature;
2013-07-03 traytel 2013-07-03 use long goal format in rel_induct theorem
2013-07-03 traytel 2013-07-03 share some code between codatatypes, datatypes and eventually prim(co)rec
2013-07-03 nipkow 2013-07-03 tuned names
2013-07-02 wenzelm 2013-07-02 tuned;
2013-07-02 wenzelm 2013-07-02 allow choice of target directory (again, see also 58e2d0cd81ae);
2013-07-02 wenzelm 2013-07-02 postinstall: recover Cygwin permissions;
2013-07-02 wenzelm 2013-07-02 clarified initial cd;
2013-07-02 wenzelm 2013-07-02 clarified Proofterm.proofs vs. Goal.skip_proofs;
2013-07-01 wenzelm 2013-07-01 clarified focus after dismiss;
2013-07-01 wenzelm 2013-07-01 tuned signature;
2013-07-01 wenzelm 2013-07-01 avoid repeated window popup when the mouse is moved over the same content (again, see also cb677987b7e3 and 0a1db0d02628);
2013-07-01 wenzelm 2013-07-01 more robust delayed invocation;
2013-07-01 wenzelm 2013-07-01 clarified tooltip timing of pending event and active state;
2013-07-01 wenzelm 2013-07-01 less intrusive border, notably on windows;
2013-07-01 wenzelm 2013-07-01 tighten tooltip size;
2013-07-01 wenzelm 2013-07-01 visually explicit focus (behaviour dependent on platform and look-and-feel);
2013-06-30 wenzelm 2013-06-30 tuned;
2013-06-30 wenzelm 2013-06-30 more uniform notion of disabled proofs -- NB: historic meaning of 1 for recording theorems is already included in 0;
2013-06-30 wenzelm 2013-06-30 discontinued system option "proofs" -- global state of Proofterm.proofs is persistently compiled into HOL-Proofs image; discontinued unused proofterms for FOL;
2013-06-30 wenzelm 2013-06-30 backout dedd7952a62c: static "proofs" value within theory prevents later inferencing with different configuration;
2013-06-30 wenzelm 2013-06-30 just one alternative proof syntax, which also works for Proof_Syntax.pretty_proof/Proof_Syntax.read_proof roundtrip;
2013-06-30 haftmann 2013-06-30 CONTRIBUTORS
2013-06-29 wenzelm 2013-06-29 avoid potential race condition of focusLost/dismiss vs. popup.show;
2013-06-29 wenzelm 2013-06-29 more direct use of screen location: avoid misplacement if parent component has already disappeared asynchronously;
2013-06-29 wenzelm 2013-06-29 explicit Pretty_Tooltip.dismiss_all due to slightly changed focus mechanics;
2013-06-29 wenzelm 2013-06-29 update text only once;
2013-06-29 wenzelm 2013-06-29 tuned signature;
2013-06-29 wenzelm 2013-06-29 more aggresive ESCAPE handling, while retaining its regular meaning for jEdit;
2013-06-29 wenzelm 2013-06-29 manage popup windows via PopupFactory, which prefers light-weight JComponent, but might fall back on JWindow (despite JPanel of 0f88591478e6); more explicit tooltip hierarchy: manage exactly the visible stack -- caching is part of PopupFactory; auxiliary geometry measurement via single hidden window; tuned signature;
2013-06-29 wenzelm 2013-06-29 tuned signature;
2013-06-29 haftmann 2013-06-29 yet another warning
2013-06-28 haftmann 2013-06-28 sort out code equations headed by a projection of a abstract datatype
2013-06-28 haftmann 2013-06-28 formally accept dictionary parameters for constants on left hand sides in equations
2013-06-28 haftmann 2013-06-28 do not choke on type variables emerging during rewriting
2013-06-28 wenzelm 2013-06-28 load icons via options -- prefer IntelliJ IDEA for now;
2013-06-28 wenzelm 2013-06-28 support for idea-icons (using ideaIC-129.354/platform/icons/src from IntelliJ IDEA Community Edition 12.1.2);
2013-06-27 wenzelm 2013-06-27 manage option "proofs" within theory context -- with minor overhead for primitive inferences;
2013-06-27 wenzelm 2013-06-27 tuned signature;
2013-06-27 wenzelm 2013-06-27 proper bold versions of 00ac (logicalnot), 00b0 (degree);
2013-06-27 wenzelm 2013-06-27 tuned signature;
2013-06-27 wenzelm 2013-06-27 merged
2013-06-27 wenzelm 2013-06-27 tuned signature;
2013-06-27 wenzelm 2013-06-27 clarified printing of type constraints vs. annotations, notably in goal display with its Type_Annotation.ignore_free_types;
2013-06-27 wenzelm 2013-06-27 updated documentation;
2013-06-27 wenzelm 2013-06-27 actually use Data.sizef, not hardwired size_of_thm;
2013-06-27 wenzelm 2013-06-27 more scalable PARALLEL_GOALS, using more elementary retrofit; tuned signature;
2013-06-27 nipkow 2013-06-27 tuned
2013-06-26 wenzelm 2013-06-26 merged
2013-06-26 wenzelm 2013-06-26 less intrusive SELECT_GOAL: merely rearrange subgoals without detaching goal state, and thus preserve maxidx context; even less intrusive PREFER_GOAL (without structural goal marker), e.g. relevant for generic_simp_tac; adapted ZF proof that broke for unknown reasons (potentially slight change of Drule.size_of_thm);
2013-06-26 wenzelm 2013-06-26 SOMEthing went utterly wrong;
2013-06-26 wenzelm 2013-06-26 tuned signature;
2013-06-26 wenzelm 2013-06-26 more position information for markup;
2013-06-26 smolkas 2013-06-26 tuned: cleaned up data structure
2013-06-26 smolkas 2013-06-26 simplified data structure
2013-06-26 smolkas 2013-06-26 ommit trivial tfrees in annotations