Mercurial
Mercurial
>
repos
>
isabelle
/ graph
summary
|
shortlog
|
changelog
| graph |
tags
|
bookmarks
|
branches
|
files
|
gz
|
help
less
more
|
(0)
-30000
-10000
-3000
-1000
-240
+240
+1000
tip
Find changesets by keywords (author, files, the commit message), revision number or hash, or
revset expression
.
The revision graph only works with JavaScript-enabled browsers.
tuned
9 months ago, by nipkow
merged
9 months ago, by nipkow
merged
9 months ago, by nipkow
merged
9 months ago, by nipkow
tuned slow proof
9 months ago, by nipkow
merged
9 months ago, by wenzelm
proper bullet symbols for GUI text -- in contrast to Isabelle \<bullet> 0x002219;
9 months ago, by wenzelm
tuned: more direct GUI painting via HTML;
9 months ago, by wenzelm
tuned generated output: more standard operations;
9 months ago, by wenzelm
tuned GUI output: more uniform;
9 months ago, by wenzelm
minor performance tuning;
9 months ago, by wenzelm
tuned generated output: more standard operations;
9 months ago, by wenzelm
clarified signature: more operations;
9 months ago, by wenzelm
more accurate treatment of plain text (amending eede0cf38a63);
9 months ago, by wenzelm
clarified signature: more operations;
9 months ago, by wenzelm
clarified signature;
9 months ago, by wenzelm
tuned, following theories_status.scala;
9 months ago, by wenzelm
tuned imports;
9 months ago, by wenzelm
tuned GUI output;
9 months ago, by wenzelm
clarified signature: ensure uniform style;
9 months ago, by wenzelm
tuned GUI output;
9 months ago, by wenzelm
clarified signature;
9 months ago, by wenzelm
tuned;
9 months ago, by wenzelm
clarified signature;
9 months ago, by wenzelm
drop redundant space in HTML (see also 18a720984855);
9 months ago, by wenzelm
clarified signature;
9 months ago, by wenzelm
more robust: proper HTML.output;
9 months ago, by wenzelm
tuned signature;
9 months ago, by wenzelm
tuned: fewer warnings in IntelliJ IDEA;
9 months ago, by wenzelm
clarified output;
9 months ago, by wenzelm
clarified signature;
9 months ago, by wenzelm
more GUI styles;
9 months ago, by wenzelm
clarified signature;
9 months ago, by wenzelm
tuned signature;
9 months ago, by wenzelm
tuned: fewer warnings in IntelliJ IDEA;
9 months ago, by wenzelm
tuned: fewer warnings in IntelliJ IDEA;
9 months ago, by wenzelm
tuned proofs;
9 months ago, by wenzelm
some bit operations on target numerals
9 months ago, by haftmann
explicit tests for target-language bit operations
9 months ago, by haftmann
avoid default simp rule which would produce strange recursive unfolding in presence of bit_eq_iff
9 months ago, by haftmann
update to xz-java-1.10 for further testing (see also fe7238c01809);
9 months ago, by wenzelm
more default simp rules
9 months ago, by haftmann
back to xz-java-1.9, to see if this improves build_manager stability;
9 months ago, by wenzelm
merged
9 months ago, by paulson
revered the hiding of the standard nat theorems
9 months ago, by paulson
minor performance tuning; directly try to read file instead of first checking its existence
9 months ago, by desharna
merged
9 months ago, by desharna
minor performance tuning; avoid constructing path if unused and double construction
9 months ago, by desharna
merged
9 months ago, by wenzelm
more markup: for diagnostic purposes of ambig_msgs;
9 months ago, by wenzelm
more uniform Markup.notation vs. Markup.expression;
9 months ago, by wenzelm
tuned output: suppress vacuous nodes from 07ad0b407d38;
9 months ago, by wenzelm
clarified LaTeX presentation: more specific keywords;
9 months ago, by wenzelm
clarified literal data;
9 months ago, by wenzelm
merged
9 months ago, by desharna
tuned ATP caching in Sledgehammer to consider the command line
9 months ago, by desharna
tuned function lines_of_atp_problem to have header lines as proper list elements
9 months ago, by desharna
tuned tests for existing directories in Sledgehammer
9 months ago, by desharna
merged
9 months ago, by wenzelm
tuned GUI: more informative search_title;
9 months ago, by wenzelm
clarified induct rules: proper case_names;
9 months ago, by wenzelm
tuned proofs;
9 months ago, by wenzelm
tuned GUI: trim text as in org.gjt.sp.jedit.search.HyperSearchResult;
9 months ago, by wenzelm
clarified GUI: more auto_hovering_button instances;
9 months ago, by wenzelm
more robust: prefer official BasicSplitPaneUI operations;
9 months ago, by wenzelm
clarified split_pane layout: close on first display, open on first search;
9 months ago, by wenzelm
more operations, specifically for FlatLaf;
9 months ago, by wenzelm
added documentation for new Sledehammer option "cache_dir"
9 months ago, by desharna
updated affiliation in Sledgehammer documentation
9 months ago, by desharna
merged
9 months ago, by desharna
added option "cache_dir" to Sledgehammer
9 months ago, by desharna
more simp rules on word conversions
9 months ago, by haftmann
spelling;
9 months ago, by wenzelm
update to xz-java-1.10;
9 months ago, by wenzelm
update to zstd-jni-1.5.6-8;
9 months ago, by wenzelm
update to sqlite-3.47.1.0;
9 months ago, by wenzelm
updated to postgresql-42.7.4;
9 months ago, by wenzelm
update to llncs-2.25;
9 months ago, by wenzelm
update to jsoup-1.18.3;
9 months ago, by wenzelm
clarified signature;
9 months ago, by wenzelm
tuned proofs;
9 months ago, by wenzelm
avoid duplicate markup, notably from "CONST c";
9 months ago, by wenzelm
clarified pretty_entity for syntax consts without mixfix annotation (see also 43c4817375bf and d622145603ee);
9 months ago, by wenzelm
tuned;
9 months ago, by wenzelm
clarified signature (see also 2157039256d3);
9 months ago, by wenzelm
more syntax bundles, e.g. to explore terms without notation;
9 months ago, by wenzelm
commands 'syntax_types' and 'syntax_consts' now work in a local theory context;
9 months ago, by wenzelm
tuned names;
9 months ago, by wenzelm
tuned signature: avoid shadowing;
9 months ago, by wenzelm
syntax translations now work in a local theory context;
9 months ago, by wenzelm
clarified signature;
9 months ago, by wenzelm
clarified signature and modules;
9 months ago, by wenzelm
minor performance tuning: avoid excessive Library.insert and Symbol.explode operations;
9 months ago, by wenzelm
tuned whitespace;
9 months ago, by wenzelm
tuned proofs;
9 months ago, by wenzelm
tuned proofs;
9 months ago, by wenzelm
clarified class/locale reasoning: avoid side-stepping constraints;
9 months ago, by wenzelm
clarified default_sort: "cpo" for bootstrap, "domain" for main HOLCF;
9 months ago, by wenzelm
clarified specification context;
9 months ago, by wenzelm
activate e-3.1 as proposed by Martin Desharnais;
9 months ago, by wenzelm
more robust: avoid spurious crash of text_area.getText() in Active_Area.update();
9 months ago, by wenzelm
proper bundle binomial_syntax;
9 months ago, by wenzelm
build component for cvc5-1.2.0;
9 months ago, by wenzelm
tuned whitespace;
9 months ago, by wenzelm
clarified default_sort;
9 months ago, by wenzelm
fewer theories;
9 months ago, by wenzelm
fewer theories;
9 months ago, by wenzelm
fewer theories (in contrast to 05ca920cd94b);
9 months ago, by wenzelm
more accurate markup for "CONST c";
9 months ago, by wenzelm
tuned markup;
9 months ago, by wenzelm
proper LaTeX setup (amending 41b387d47739);
9 months ago, by wenzelm
more LaTeX markup for printed entities;
9 months ago, by wenzelm
tuned;
9 months ago, by wenzelm
tuned;
9 months ago, by wenzelm
more HTML markup (without rendering);
9 months ago, by wenzelm
more markup (without rendering): class, type constructor, term constant --- similar to free, bound, etc.;
9 months ago, by wenzelm
tuned: more robust wrt. changes the Markup space;
9 months ago, by wenzelm
tuned: prefer explicit names of inferred types;
9 months ago, by wenzelm
more accurate HTML markup: suppress text_color that has_syntax (amending b57996a0688c);
9 months ago, by wenzelm
clarified signature;
9 months ago, by wenzelm
tuned;
9 months ago, by wenzelm
clarified signature;
9 months ago, by wenzelm
clarified term positions and markup: syntax = true means this is via concrete syntax;
9 months ago, by wenzelm
tuned signature: more operations;
9 months ago, by wenzelm
tuned;
9 months ago, by wenzelm
clarified signature: more explicit operations;
9 months ago, by wenzelm
tuned;
9 months ago, by wenzelm
tuned whitespace;
9 months ago, by wenzelm
clarified signature and caching;
9 months ago, by wenzelm
clarified GUI: prefer user documents, which are typically without chapter;
9 months ago, by wenzelm
tuned;
9 months ago, by wenzelm
obsolete;
9 months ago, by wenzelm
tuned signature;
9 months ago, by wenzelm
merged
9 months ago, by wenzelm
NEWS;
9 months ago, by wenzelm
clarified renaming of bounds, using Syntax_Trans.variant_bounds: avoid structures and fixed variables with syntax;
9 months ago, by wenzelm
tuned signature;
9 months ago, by wenzelm
clarified printing of consts: rename apart from all bounds, and thus avoid old Term.declare_free_names with its adhoc policy ("as they are printed");
9 months ago, by wenzelm
prefer Term.variant_bounds: bounds vs. frees, no attempt at consts;
10 months ago, by wenzelm
more elementary operation Term.variant_bounds: only for bounds vs. frees, no consts, no tfrees;
10 months ago, by wenzelm
tuned signature;
10 months ago, by wenzelm
clarified modules;
10 months ago, by wenzelm
more accurate extern_const: avoid clash with frees;
10 months ago, by wenzelm
more direct Proof_Context.lookup_free -- bypass redundancy of Proof_Context.check_const;
10 months ago, by wenzelm
clarified signature: uniform context;
10 months ago, by wenzelm
clarified signature: uniform context;
10 months ago, by wenzelm
proper context for extern operation: observe local options;
10 months ago, by wenzelm
proper context for extern/check operation: observe local options like names_unique;
10 months ago, by wenzelm
tuned;
10 months ago, by wenzelm
tuned signature: more operations;
10 months ago, by wenzelm
added Halting problem theory
10 months ago, by nipkow
merged
10 months ago, by desharna
added parallel_group_size option to Mirabelle
2023-09-29, by desharna
adapted bash files to use cartouches
10 months ago, by desharna
tuned
10 months ago, by nipkow
clarified names context: proper context, without consts;
10 months ago, by wenzelm
clarified names context: proper context, without consts;
10 months ago, by wenzelm
tuned;
10 months ago, by wenzelm
tuned;
10 months ago, by wenzelm
clarified signature: more operations;
10 months ago, by wenzelm
merged
10 months ago, by wenzelm
clarified signature;
10 months ago, by wenzelm
tuned names/scopes;
10 months ago, by wenzelm
tuned signature: more operations;
10 months ago, by wenzelm
eliminate historic clone (see also 550e36c6a2d1);
10 months ago, by wenzelm
tuned signature: more operations;
10 months ago, by wenzelm
clarified 'unbundle' polarity, according to algebraic group laws;
10 months ago, by wenzelm
tuned signature: more operations;
10 months ago, by wenzelm
tuned: more direct use of Name.context operations;
10 months ago, by wenzelm
tuned;
10 months ago, by wenzelm
misc tuning and clarification: more direct use of Name.context operations;
10 months ago, by wenzelm
tuned signature: more operations;
10 months ago, by wenzelm
tuned: more direct use of Name.context operations;
10 months ago, by wenzelm
clarified signature: shorten common cases;
10 months ago, by wenzelm
tuned: more standard Name.build_context, although that is a bit longer;
10 months ago, by wenzelm
clarified signature: more uniform;
10 months ago, by wenzelm
omit redundant combinators (amending 7456a64bc4f6);
10 months ago, by wenzelm
tuned signature;
10 months ago, by wenzelm
fixed bugs found by Stepan Holub
10 months ago, by blanchet
merged
10 months ago, by nipkow
added lemmas
10 months ago, by nipkow
merged
10 months ago, by wenzelm
more ambitious Search_Result.gui_text, using Swing HTML3 (NB: TreeCellRenderer cannot do this, because it is not updated for each entry);
10 months ago, by wenzelm
clarified signature and object initialization;
10 months ago, by wenzelm
clarified default: avoid copies;
10 months ago, by wenzelm
suppress odd icons for documents and folders;
10 months ago, by wenzelm
support for modified tree cell renderer;
10 months ago, by wenzelm
clarified signature: avoid implicit functionality;
10 months ago, by wenzelm
re-use Output_Area;
10 months ago, by wenzelm
re-use Output_Area;
10 months ago, by wenzelm
re-use Output_Area;
10 months ago, by wenzelm
re-use Output_Area with search results;
10 months ago, by wenzelm
re-use Output_Area with search results;
10 months ago, by wenzelm
more thorough init;
10 months ago, by wenzelm
clarified signature: prefer defaults for Output_Dockable (and its variants);
10 months ago, by wenzelm
unused;
10 months ago, by wenzelm
tuned output: formatting is pointless for proportional font;
10 months ago, by wenzelm
clarified Tree_View.init_model: more uniform;
10 months ago, by wenzelm
more robust update;
10 months ago, by wenzelm
handle tree selection;
10 months ago, by wenzelm
Output_Dockable: show search results as tree view;
10 months ago, by wenzelm
clarified modules;
10 months ago, by wenzelm
clarified signature;
10 months ago, by wenzelm
clarified signature;
10 months ago, by wenzelm
clarified signature and modules: without GUI change yet;
10 months ago, by wenzelm
more operations, to support search within output panel;
10 months ago, by wenzelm
tuned;
10 months ago, by wenzelm
Introduced the function some_elem for grabbing an element from a non-empty set, and simplified the theorem the_elem_image_unique
10 months ago, by paulson
Patch by Stepan Holub, plus tweaks
10 months ago, by paulson
patch to vector_matrix_mult by Alexander Pach
10 months ago, by paulson
try0: cleaned up output;
10 months ago, by Fabian Huch
try0: insert extra facts into state instead of goal, since some methods (e.g. metis) won't work otherwise;
10 months ago, by Fabian Huch
avoid informatik.tu-muenchen.de domain: soon to be discontinued;
10 months ago, by Fabian Huch
renamed Discrete -> Discrete_Functions to avoid name clashes;
10 months ago, by nipkow
Use Var to maintain the difference between function and locale parameters
10 months ago, by nipkow
tuned
10 months ago, by nipkow
tuned proofs;
10 months ago, by wenzelm
tuned proofs;
10 months ago, by wenzelm
minor performance tuning: avoided repeated metric initialization;
10 months ago, by wenzelm
tuned signature: more operations;
10 months ago, by wenzelm
clarified signature;
10 months ago, by wenzelm
more NEWS;
10 months ago, by wenzelm
tuned proofs;
10 months ago, by wenzelm
merged
10 months ago, by wenzelm
enforce rebuild of Isabelle/ML and Isabelle/Scala;
10 months ago, by wenzelm
update to jedit-20241115 (see also ecd62f7b3644 and d92d754b5dd9);
10 months ago, by wenzelm
more patches for the sake of SideKick 1.8 vs. jEdit 5.7.0: provide missing GUIUtilities.isPopupTrigger, avoid StatusBar messages (which often don't fit);
10 months ago, by wenzelm
tuned comments;
10 months ago, by wenzelm
clarified key events: cancel output selection, before input selection;
10 months ago, by wenzelm
proper focus to support subsequent copy-paste via keyboard;
10 months ago, by wenzelm
more accurate initial FontRenderContext, notably on macOS, Windows, or Linux with "env GDK_SCALE=2";
10 months ago, by wenzelm
removed obsolete option: jEdit 5.7.0 can be built with default jdk;
10 months ago, by wenzelm
more rebust mechanics of refresh (see also 82110cbcf9a1 and 2d9b6e32632d): painter.getFontRenderContext might be in undefined state (notably on macOS due to display scaling);
10 months ago, by wenzelm
less ambitious selection;
10 months ago, by wenzelm
mv Discrete to Discrete_Cpo to avoid theory name clashes
10 months ago, by nipkow
disable 2d9b6e32632d for now: unknown problems on macOS;
10 months ago, by wenzelm
clarified mouse selection, avoid conflict of double-click with single-click (follow hyperlink);
10 months ago, by wenzelm
more careful isConsumed() / consume() for key and mouse events;
10 months ago, by wenzelm
merged
10 months ago, by nipkow
added field input_eqns to record the list of equations (the specification)
10 months ago, by nipkow
less
more
|
(0)
-30000
-10000
-3000
-1000
-240
+240
+1000
tip