isabelle: Graph

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

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;
9 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
9 months ago, by nipkow
merged
9 months ago, by desharna
added parallel_group_size option to Mirabelle
2023-09-29, by desharna
adapted bash files to use cartouches
9 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