isabelle: Graph

Mercurial Mercurial > repos > isabelle / graph

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

Added tag Isabelle2021-1-RC5 for changeset 8baf2e8b16e2
16 months ago, by wenzelm
more documentation about Type/Const antiquotations;
16 months ago, by wenzelm
more documentation about document build options;
16 months ago, by wenzelm
address problems with launch4j and jdk-17 (see also 41d009462d3c, copy of 41d009462d3c);
16 months ago, by wenzelm
tuned --- fewer IDE warnings;
16 months ago, by wenzelm
more robust physical timeout (despite 1bea05713dde), especially relevant for quickcheck where large unary numerals may cause excessive heap allocations and resulting GC is better included in the timing;
16 months ago, by wenzelm
added definitions multp{DM,HO} and corresponding lemmas
16 months ago, by desharna
added wfP_less to wellorder and wfP_less_multiset
16 months ago, by desharna
restored lemmas less_multiset{DM,HO} inadvertently changed by c256bba593f3
16 months ago, by desharna
merged
16 months ago, by desharna
added lemmas irreflp_{less,greater} to preorder and {trans,irrefl}_mult{,p} to Multiset
16 months ago, by desharna
redefined less_multiset to be based on multp
16 months ago, by desharna
added lemmas multp_code_eq_multp and multeqp_code_eq_reflclp_multp
16 months ago, by desharna
added lemmas multp_cancel, multp_cancel_add_mset, and multp_cancel_max
16 months ago, by desharna
added lemmas multp_implies_one_step, one_step_implies_multp, and subset_implies_multp
16 months ago, by desharna
added lemma wfP_multp
16 months ago, by desharna
added lemma mono_multp
16 months ago, by desharna
added Multiset.multp as predicate equivalent of Multiset.mult
16 months ago, by desharna
address problems with launch4j and jdk-17 (see also 41d009462d3c);
16 months ago, by wenzelm
more robust build on midrange hardware;
16 months ago, by wenzelm
clarified tests: omit somewhat pointless (unstable) results;
16 months ago, by wenzelm
proper fields for gnuplot (amending b614e3e4146a);
16 months ago, by wenzelm
tuned output;
16 months ago, by wenzelm
tuned;
16 months ago, by wenzelm
merged
16 months ago, by wenzelm
more robust build on midrange hardware (despite 67d6f1708ea4);
16 months ago, by wenzelm
Added tag Isabelle2021-1-RC4 for changeset 2336356d4180
16 months ago, by wenzelm
updated to polyml-5.9;
16 months ago, by wenzelm
NEWS on "isabelle mirabelle";
16 months ago, by wenzelm
tuned;
16 months ago, by wenzelm
clarified default for kodkod_scala;
16 months ago, by wenzelm
maintain option kodkod_scala within theory context, to allow local modification;
16 months ago, by wenzelm
NEWS for proper release;
16 months ago, by wenzelm
updated to flatlaf-1.6.4;
16 months ago, by wenzelm
avoid broken links: auxiliary files are not yet supported;
16 months ago, by wenzelm
option document_comment_latex supports e.g. Dagstuhl LIPIcs;
16 months ago, by wenzelm
more explicit type Latex.Tags;
16 months ago, by wenzelm
more uniform treatment of optional_argument for Latex elements;
16 months ago, by wenzelm
removed pointless 'text_cartouche' command: regular 'text' already supports cartouches;
16 months ago, by wenzelm
example: alternative document headings, based on more general document output markup;
16 months ago, by wenzelm
more general document output: enclosing markup is defined in user-space;
16 months ago, by wenzelm
clarified modules (see c299abcf7081);
16 months ago, by wenzelm
output for document commands like 'section', 'text' is defined in user-space, as part of the command transaction;
16 months ago, by wenzelm
clarified modules;
16 months ago, by wenzelm
tuned signature: more explicit types for presentation;
16 months ago, by wenzelm
more robust support for Windows line-endings;
16 months ago, by wenzelm
source positions for document markup commands, e.g. to retrieve PIDE markup in presentation;
16 months ago, by wenzelm
more compact data during presentation: Entity_Context.Theory_Export instead of full Export_Theory.Theory;
16 months ago, by wenzelm
clarified system option standard values: avoid oddities like "isabelle build -o document_output" producing directories named "true";
16 months ago, by wenzelm
more symbolic latex_output via XML (using YXML within text);
16 months ago, by wenzelm
proper enclose_name (amending e77c5bfca9aa);
16 months ago, by wenzelm
Latex.Output.latex_heading depends on option document_heading_prefix, e.g. relevant for Dagstuhl LIPIcs which prefers unaliased \section etc.;
16 months ago, by wenzelm
more symbolic latex_output via XML;
16 months ago, by wenzelm
clarified hook for Mirabelle (again): cover all 'theories' sections within ROOT (see also 9ead8d9be3ab);
16 months ago, by wenzelm
tuned;
16 months ago, by wenzelm
tuned;
16 months ago, by wenzelm
updated to verit-2021.06.2-rmx;
16 months ago, by wenzelm
clarified HTML_Context.theory_exports: prefer value-oriented parallelism;
16 months ago, by wenzelm
generate problems with correct logic for veriT
16 months ago, by fleury
more parallelism, at the cost of potential duplicates of make_thy;
16 months ago, by wenzelm

less more | (0) -30000 -10000 -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 tip

isabelle