isabelle: Graph

added field input_eqns to record the list of equations (the specification)
5 months ago, by nipkow
merged
5 months ago, by wenzelm
more NEWS;
5 months ago, by wenzelm
tuned proofs;
5 months ago, by wenzelm
more ambitious mouse handler: double-click selects highlight_area;
5 months ago, by wenzelm
more accurate mouse handler: only for single clicks, consume accepted event;
5 months ago, by wenzelm
more ambitious scrolling: retain original scroll position if possible;
5 months ago, by wenzelm
more ambitious scrolling: retain bottom position after output;
5 months ago, by wenzelm
performance tuning: cache for Rich_Text.format, notably for incremental tracing;
5 months ago, by wenzelm
clarified persistent values: Command.Results does not suitable for caching, because it contains all other messages;
5 months ago, by wenzelm
omit redundant compact_source (see e1abca2527da): Command_Span.unparsed consists of one token with the original source;
5 months ago, by wenzelm
tuned;
5 months ago, by wenzelm
minor performance tuning: avoid duplication of Symbol.spaces (e.g. from Pretty.formatted);
5 months ago, by wenzelm
clarified signature and modules;
5 months ago, by wenzelm
performance tuning for macOS (after update of "jedit" component): old OpenGL works better for text rendering;
5 months ago, by wenzelm
performance tuning: more incremental update of buffer content;
5 months ago, by wenzelm
obsolete;
5 months ago, by wenzelm
clarified: more uniform results;
5 months ago, by wenzelm
clarified signature: inline org.gjt.sp.jedit.textarea.TextArea.setText();
5 months ago, by wenzelm
minor performance tuning: avoid concatenation of existing string material;
5 months ago, by wenzelm
clarified signature and data storage: incremental lazy values;
5 months ago, by wenzelm
tuned comments;
5 months ago, by wenzelm
clarified signature;
5 months ago, by wenzelm
clarified modules;
5 months ago, by wenzelm
clarified margin operations (again, reverting 4794576828df);
5 months ago, by wenzelm
clarified modules;
5 months ago, by wenzelm
more reactive interrupts (via Future.cancel);
5 months ago, by wenzelm
Document.Snapshot: support for multiple snippet_commands;
5 months ago, by wenzelm
more robust: make double-sure that this is the correct output, not a different version from concurrent GUI_Thread.later;
5 months ago, by wenzelm
clarified signature: include standard margin in object equality;
5 months ago, by wenzelm
performance tuning: prefer asynchronous Pretty.formatted, which actually takes longer than Command.rich_text (see also 97964515a676, where Pretty.formatted was on the GUI thread, maybe for the sake of java.awt.FontMetrics at that time);
5 months ago, by wenzelm
The ceillog2 function (thanks to Manuel Eberl), replacing two copies of Ceil_Log2
5 months ago, by paulson
merged
5 months ago, by wenzelm
merged
5 months ago, by wenzelm
clarified signature: avoid pointless alias (see also c82a1620b274 and 22aeec526ffd);
5 months ago, by wenzelm
clarified signature;
5 months ago, by wenzelm
tuned GUI: avoid wasting space with proportional fonts;
5 months ago, by wenzelm
clarified signature;
5 months ago, by wenzelm
more accurate pretty_margin for proportional fonts;
5 months ago, by wenzelm
clarified signature: more uniform;
5 months ago, by wenzelm
tuned: fewer warnings in IntelliJ IDEA;
5 months ago, by wenzelm
tuned signature;
5 months ago, by wenzelm
tuned signature;
5 months ago, by wenzelm
clarified signature with subtle change of semantics: output consists of individual messages that are formatted (and separated) internally;
5 months ago, by wenzelm
more accurate message boundaries;
5 months ago, by wenzelm
tuned whitespace;
5 months ago, by wenzelm
clarified signature: more robust type XML.Elem;
5 months ago, by wenzelm
clarified signature;
5 months ago, by wenzelm
clarified signature;
5 months ago, by wenzelm
clarified output representation: postpone Pretty.separate;
5 months ago, by wenzelm
tuned;
5 months ago, by wenzelm
tuned: fewer warnings in IntelliJ IDEA;
5 months ago, by wenzelm
clarified signature: more accurate types;
5 months ago, by wenzelm
tuned signature: more standard names;
5 months ago, by wenzelm
more uniform pretty_text_area.zoom via its zoom_component;
5 months ago, by wenzelm
tuned signature;
5 months ago, by wenzelm
tuned signature: more standard names;
5 months ago, by wenzelm
tuned;
5 months ago, by wenzelm
clarified signature;
5 months ago, by wenzelm
clarified signature;
5 months ago, by wenzelm
tuned;
5 months ago, by wenzelm
revert 1206400b9b48: proper Node.unapply for Node.apply(null);
5 months ago, by wenzelm
tuned signature;
5 months ago, by wenzelm
clarified signature;
5 months ago, by wenzelm
clarified signature, with subtle change of semantics: proper non-null result;
5 months ago, by wenzelm
clarified modules;
5 months ago, by wenzelm
more robust and uniform metric, still with special treatment motivated by jEdit (see also 0cdfce0bf956);
5 months ago, by wenzelm
misc tuning;
5 months ago, by wenzelm
try0: avoid mapping background theory -- should be handled by Context_Position visibility;
5 months ago, by Fabian Huch
try0: stop early if more subgoals are created;
5 months ago, by Fabian Huch
try0: filter out untagged thms;
5 months ago, by Fabian Huch
try0: support literal facts;
5 months ago, by Fabian Huch
try0: add 'use' modifier for thms to insert;
5 months ago, by Fabian Huch
try0: use extra thms via insert;
5 months ago, by Fabian Huch
clarified: proper type for facts;
5 months ago, by Fabian Huch
clarified: proper type;
5 months ago, by Fabian Huch
tuned;
6 months ago, by Fabian Huch
tuned;
6 months ago, by Fabian Huch
try0: pass tagged thms for better control;
6 months ago, by Fabian Huch
clarified: proper return type;
6 months ago, by Fabian Huch
improve try0: solve multiple subgoals at once, if possible;
6 months ago, by Fabian Huch
tuned: unused parameter;
6 months ago, by Fabian Huch
tuned
5 months ago, by nipkow
better termination behaviour
5 months ago, by nipkow
uniform name T_f for closed-form lemmas for function T_f
5 months ago, by nipkow
More time for primitive functions
5 months ago, by nipkow
merged Reverse into Time_Funs
5 months ago, by nipkow
tuned proofs;
5 months ago, by wenzelm
tuned description: plain text documentation is also supported;
5 months ago, by wenzelm
merged
5 months ago, by wenzelm
update to jdk-21.0.5;
5 months ago, by wenzelm
misc tuning and clarification: Doc.Entry supports both plain files and pdf documents;
5 months ago, by wenzelm
tuned proofs
5 months ago, by nipkow
added missing definitions
5 months ago, by nipkow
tuned proofs;
5 months ago, by wenzelm
clarified modules;
5 months ago, by wenzelm
support value-oriented Font_Metric, e.g. for caching Pretty output;
5 months ago, by wenzelm
tuned;
5 months ago, by wenzelm
unused;
5 months ago, by wenzelm
tuned;
5 months ago, by wenzelm
tuned;
5 months ago, by wenzelm
clarified signature;
5 months ago, by wenzelm
more accurate Symbol.Metric, following 6eccae338770;
5 months ago, by wenzelm
tuned rendering, notably for HiDPI on Linux (see also ca7e2c21b104);
5 months ago, by wenzelm
proper parentheses, for the sake of IntelliJ IDEA;
5 months ago, by wenzelm
clarified modules;
5 months ago, by wenzelm
clarified signature;
5 months ago, by wenzelm
tuned proofs;
5 months ago, by wenzelm
tuned GUI (again, see 0521e65af41e);
5 months ago, by wenzelm
tuned proofs;
5 months ago, by wenzelm
tuned;
5 months ago, by wenzelm
tuned comments;
5 months ago, by wenzelm
clarified signature;
5 months ago, by wenzelm
tuned;
5 months ago, by wenzelm
tuned names;
5 months ago, by wenzelm
more robust;
5 months ago, by wenzelm
clarified signature;
5 months ago, by wenzelm
unused;
5 months ago, by wenzelm
clarified signature: more explicit types;
5 months ago, by wenzelm
tuned GUI;
5 months ago, by wenzelm
tuned;
5 months ago, by wenzelm
clarified signature;
5 months ago, by wenzelm
clarified signature;
5 months ago, by wenzelm
tuned imports;
5 months ago, by wenzelm
tuned: remove redundant checks;
5 months ago, by wenzelm
tuned;
5 months ago, by wenzelm
clarified modules;
5 months ago, by wenzelm
clarified signature;
5 months ago, by wenzelm
clarified signature;
5 months ago, by wenzelm
clarified signature;
5 months ago, by wenzelm
tuned: fewer warnings in IntelliJ IDEA;
5 months ago, by wenzelm
clarified signature;
5 months ago, by wenzelm
clarified modules: more re-usable;
5 months ago, by wenzelm
proper protocol messages (amending 7a1f9e571046);
5 months ago, by wenzelm
clarified treatment of caret_range: better support for multiple (unrelated) selections;
5 months ago, by wenzelm
tuned whitespace;
5 months ago, by wenzelm
support incremental isabelle.select-structure --- like select-block, but based on selection instead of caret;
5 months ago, by wenzelm
clarified rendering: entity acts as atomic notation / expression;
5 months ago, by wenzelm
more rendering for Markup.COMMAND_SPAN, following Rendering.structure_elements;
5 months ago, by wenzelm
more NEWS;
5 months ago, by wenzelm
merged
5 months ago, by wenzelm
support Isabelle/jEdit action isabelle.select_structure;
5 months ago, by wenzelm
more operations;
5 months ago, by wenzelm
clarified text;
5 months ago, by wenzelm
update to jedit5.7.0;
5 months ago, by wenzelm
GUI option "editor_auto_hovering" for Output panel;
5 months ago, by wenzelm
update to scala-3.3.4 LTS;
5 months ago, by wenzelm
removed obsolete markup for "open_block" (see also d5ad89fda714): Isabelle/Scala directly supports XML.Elem pretty-printing;
5 months ago, by wenzelm
Library material from Eberl's Parallel_Shear_Sort
5 months ago, by paulson
Trying to clean up these horribly ugly old proofs, but the requirement of constructivity makes it very difficult
5 months ago, by paulson
use automatically generated time function in HOL-Data_Structures.Selection
5 months ago, by Manuel Eberl
merged
5 months ago, by nipkow
better time_functions (let)
5 months ago, by nipkow
less hidden configuration;
5 months ago, by Fabian Huch
proper passwordless smtp check: must be null;
5 months ago, by Fabian Huch
adjusted documentation
5 months ago, by blanchet
more attribute tuning
5 months ago, by nipkow
tuned attributes
5 months ago, by nipkow
merged
5 months ago, by nipkow
added lemmas
5 months ago, by nipkow
tuned proofs;
5 months ago, by wenzelm
tuned NEWS;
5 months ago, by wenzelm
markup for "..." notation;
5 months ago, by wenzelm
more robust: avoid non-authentic translations;
5 months ago, by wenzelm
tuned whitespace of sources;
5 months ago, by wenzelm
update documentation;
5 months ago, by wenzelm
tuned;
5 months ago, by wenzelm
update documentation: print mode "latex" only affects syntax tables, but output of symbols;
5 months ago, by wenzelm
misc tuning and clarification;
5 months ago, by wenzelm
clarified section structure;
5 months ago, by wenzelm
tuned;
5 months ago, by wenzelm
tuned;
5 months ago, by wenzelm
tuned;
5 months ago, by wenzelm
tuned signature;
5 months ago, by wenzelm
clarified symbolic output: avoid redundant "block" element for open_block = true;
5 months ago, by wenzelm
clarified signature;
5 months ago, by wenzelm
clarified (again): Markup.intensify is already part of Variable.markup_fixed for undeclared variable, Markup.fixed is already part of Mariable.markup;
5 months ago, by wenzelm
more accurate Symbol.length;
5 months ago, by wenzelm
tuned;
5 months ago, by wenzelm
merged
5 months ago, by wenzelm
more inner-syntax markup;
5 months ago, by wenzelm
obsolete (see a8502d492dde);
5 months ago, by wenzelm
minor performance tuning;
5 months ago, by wenzelm
tuned proofs;
5 months ago, by wenzelm
more inner-syntax markup;
5 months ago, by wenzelm
merged
5 months ago, by nipkow
time_fun: lambdas and lets work now
5 months ago, by nipkow
variable instantiation in Sledgehammer and Metis
5 months ago, by blanchet
prefer rewrite_term_yoyo for improved performance and occasionally better results (conforming to Ast.normalize);
5 months ago, by wenzelm
revert b35c2aa05fcf: redundant due to 89ea66c2045b, if object-logic judgment lacks delimiters;
6 months ago, by wenzelm
clarified position constraints: omit redundant information, e.g. for implicit object-logic judgment;
6 months ago, by wenzelm
unused (see 0199acc01aa8);
6 months ago, by wenzelm
tuned;
6 months ago, by wenzelm
more robust: avoid ambiguity of contract_abbrevs;
6 months ago, by wenzelm
misc tuning: more concise (or hermetic) pointfree style;
6 months ago, by wenzelm
provide rewrite_term_yoyo, which is analogous to Ast.normalize;
6 months ago, by wenzelm
tuned signature;
6 months ago, by wenzelm
tuned names;
6 months ago, by wenzelm
tuned;
6 months ago, by wenzelm
misc tuning and clarification;
6 months ago, by wenzelm
tuned;
6 months ago, by wenzelm
misc tuning and clarification;
6 months ago, by wenzelm
merged
6 months ago, by wenzelm
adhoc option to disable const constraints, notably for AFP/Isabelle_DOF;
6 months ago, by wenzelm
unused;
6 months ago, by wenzelm
tuned signature;
6 months ago, by wenzelm
proper treatment of position constraints;
6 months ago, by wenzelm
more liberal ast matching, notably for case-translations in HOLCF that operate on logical consts rather than syntax consts;
6 months ago, by wenzelm
more parser markup, based on position constraints for logical mixfix syntax;
6 months ago, by wenzelm
more concise representation of term positions;
6 months ago, by wenzelm
more robust;
6 months ago, by wenzelm
tuned signature;
6 months ago, by wenzelm
tuned comments;
6 months ago, by wenzelm
misc tuning and clarification;
6 months ago, by wenzelm
clarified concrete vs. abstract syntax: avoid translations on logical consts;
6 months ago, by wenzelm
misc tuning and clarification;
6 months ago, by wenzelm
clarified markers for syntax consts: avoid overlap with logical consts;
6 months ago, by wenzelm
update ci mail address;
6 months ago, by Fabian Huch
minor performance tuning;
6 months ago, by wenzelm
notable performance tuning (amending a59d9b81be24 and 8976c5bc9e97): avoid costly could_beta_eta_contract, which traverses the whole term;
6 months ago, by wenzelm
tuned;
6 months ago, by wenzelm
clarified signature;
6 months ago, by wenzelm
tuned whitespace;
6 months ago, by wenzelm
support multiple positions (non-empty list);
6 months ago, by wenzelm
more robust syntax translation;
6 months ago, by wenzelm
clarified concrete vs. abstract syntax;
6 months ago, by wenzelm
more inner-syntax markup;
6 months ago, by wenzelm
clarified concrete vs. abstract syntax;
6 months ago, by wenzelm
clarified concrete vs. abstract syntax;
6 months ago, by wenzelm
more operations;
6 months ago, by wenzelm
tuned;
6 months ago, by wenzelm
tuned signature;
6 months ago, by wenzelm
more operations;
6 months ago, by wenzelm
more accurate treatment of constraints: restrict permissive mode to output;
6 months ago, by wenzelm
tuned;
6 months ago, by wenzelm
tuned proofs;
6 months ago, by wenzelm
clarified order of tooltips: make it less dependent on report order from ML (which differs for input vs. output);
6 months ago, by wenzelm
clarified signature (see also 1de8a8b1ae79);
6 months ago, by wenzelm
clarified signature;
6 months ago, by wenzelm
more type information;
6 months ago, by wenzelm