Mercurial
Mercurial
>
repos
>
isabelle
/ graph
summary
|
shortlog
|
changelog
| graph |
tags
|
bookmarks
|
branches
|
files
|
gz
|
help
less
more
|
(0)
-30000
-10000
-3000
-1000
-480
+480
+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.
clarified modules, following Isabelle/ML;
11 months ago, by wenzelm
clarified signature;
11 months ago, by wenzelm
tuned comments;
11 months ago, by wenzelm
merged
11 months ago, by paulson
the syntax of Lebesgue integrals (LINT, LBINT, ∫, etc.) now requires parentheses
11 months ago, by paulson
merged
11 months ago, by paulson
A few lemmas brought in from AFP entries
11 months ago, by paulson
merged
11 months ago, by traytel
made destructor-view tactic more robust (by Jan van Brügge)
11 months ago, by traytel
performance optimization;
11 months ago, by Fabian Huch
clarified names;
11 months ago, by Fabian Huch
clarified scheduler: proper split into scheduler, generator, and priority rules (following 32d00ec387f4);
11 months ago, by Fabian Huch
proper "linux_arm", amending 76ad72736e9e;
11 months ago, by wenzelm
more lemmas
11 months ago, by haftmann
new lemmas involving Ramsey numbers, infinite sets
11 months ago, by paulson
simplified class specification
11 months ago, by haftmann
Removal of duplicate code
11 months ago, by paulson
Two new theorems
11 months ago, by paulson
more lemmas and more correct lemma names
11 months ago, by haftmann
NEWS: corrected the definition of convexity of functions
11 months ago, by paulson
Further lemmas concerning complexity and measures
11 months ago, by paulson
Correct the definition of a convex function, and updated the proofs
11 months ago, by paulson
merged;
11 months ago, by wenzelm
update to windows_app-20240205, with executables for linux, linux_arm, macos;
11 months ago, by wenzelm
omit redundant options;
11 months ago, by wenzelm
tuned README;
11 months ago, by wenzelm
uniform build of binutils for linux, linux_arm, macos;
11 months ago, by wenzelm
fix reconstruction of Alethe's and_pos rule
12 months ago, by Mathias Fleury
added lemmas Multiset.transp_on_multp and Multiset.trans_on_mult
11 months ago, by desharna
proper target option, following package binutils-mingw-w64-x86-64 from Debian/Ubuntu;
11 months ago, by wenzelm
updated windows_app based on launch4j-3.50-linux-x64, without rebuilding GNU binutils (missing COFF target pe-i386);
11 months ago, by wenzelm
proper sfx_archive_name;
11 months ago, by wenzelm
clarified options;
11 months ago, by wenzelm
more robust;
11 months ago, by wenzelm
build Isabelle windows_app component from GNU binutils and launch4j;
11 months ago, by wenzelm
proper windows_app/launch4j-linux_arm;
11 months ago, by wenzelm
merged
11 months ago, by paulson
A small number of new lemmas
11 months ago, by paulson
explicit reference to code_dt
11 months ago, by haftmann
made lift_bnf more robust for abstract types with 'phantom' type variables
11 months ago, by traytel
rebuild "verit" for arm64-linux for more robustness, e.g. relevant for theory "HOL-ex.BigO";
11 months ago, by wenzelm
proper os_name "linux" instead of "linux_arm" (amending a33a6e541cbb);
11 months ago, by wenzelm
proper bash syntax (amending 0631dfc0db07);
11 months ago, by wenzelm
tuned proof: avoid z3;
11 months ago, by wenzelm
tuned proof: avoid z3 to make it work on arm64-linux;
11 months ago, by wenzelm
tuned proofs --- avoid smt with external prover, which is somewhat unstable on arm64-linux;
11 months ago, by wenzelm
merged
11 months ago, by wenzelm
more robust check of ISABELLE_PLATFORM_FAMILY within settings environment, to support its reunification with Isabelle/Scala (see also a33a6e541cbb, f3a356c64193);
11 months ago, by wenzelm
strengthened class parity
11 months ago, by haftmann
proper accessible paths for web server;
11 months ago, by wenzelm
more informative message (amending b8a6b2ec85a2);
11 months ago, by wenzelm
merged
11 months ago, by wenzelm
more robust: do not affect "$ISABELLE_HOME_USER/contrib" on master node;
11 months ago, by wenzelm
avoid excessive ML heap on this 16GB node;
11 months ago, by wenzelm
more robust (amending c9774306a879);
11 months ago, by wenzelm
proper ISABELLE_PLATFORM_FAMILY within Isabelle/Scala, in contrast to historic settings;
11 months ago, by wenzelm
clarified symbolic host name;
11 months ago, by wenzelm
allow remote_build on this host (server-arm), without conflicts of this "isabelle_self";
11 months ago, by wenzelm
more robust message;
11 months ago, by wenzelm
A few more new theorems taken from AFP entries
11 months ago, by paulson
merged
11 months ago, by nipkow
define_time_function: avoid unused let's
11 months ago, by nipkow
common type class for trivial properties on div/mod
11 months ago, by haftmann
more robust (amending 1600fb749c54), to support the following corner case:
11 months ago, by wenzelm
proper test options;
11 months ago, by wenzelm
proper history_base for linux_arm;
11 months ago, by wenzelm
updated to PostgreSQL 12 on Ubuntu 20.04;
11 months ago, by wenzelm
routine build + test for linux_arm;
11 months ago, by wenzelm
disable test on "augsburg1": machine will be dismantled;
11 months ago, by wenzelm
add approximation factors in build schedule to estimate build times more conservatively;
11 months ago, by Fabian Huch
merged
11 months ago, by paulson
Type class patch suggested by Achim Brucker, plus tidied lemma
11 months ago, by paulson
rearranged and reformulated abstract classes for bit structures and operations
11 months ago, by haftmann
Three new lemmas
11 months ago, by paulson
tuned proof: avoid z3 to make it work on arm64-linux;
11 months ago, by wenzelm
update to jdk-21.0.2;
11 months ago, by wenzelm
make build process state protected to avoid copying in subclasses (e.g. for database connections);
11 months ago, by Fabian Huch
add build_sync tag to sync certain options (e.g., build_engine) across build processes;
11 months ago, by Fabian Huch
clarified Mercurial version: presumably the last version that supports both python2 and python3;
11 months ago, by wenzelm
more robust: avoid crash on non-Linux systems;
11 months ago, by wenzelm
clarified webserver names;
11 months ago, by wenzelm
proper Apache.php_name;
11 months ago, by wenzelm
proper packages for mercurial_setup on Ubuntu 22.04: building from source provides hgweb modules, and also provides a defined version (6.1.1 is also provided by Ubuntu 22.04);
11 months ago, by wenzelm
tuned source structure;
11 months ago, by wenzelm
more robust systemd configuration;
11 months ago, by wenzelm
more robust nginx configuration, notably for "certbot --nginx -d DOMAIN";
11 months ago, by wenzelm
tuned whitespace in generated file;
11 months ago, by wenzelm
tuned;
11 months ago, by wenzelm
clarified modules;
11 months ago, by wenzelm
recover Url.is_wellformed from before d8330439823a, e.g. relevant for JEdit_Resources.read_file_content (the URI alone does not necessarily have a protocol prefix, so plain file-path would be treated as URL);
11 months ago, by wenzelm
proper php-fpm configuration for nginx;
11 months ago, by wenzelm
support multiple webservers: Apache or Nginx;
11 months ago, by wenzelm
tuned;
11 months ago, by wenzelm
clarified signature: explicit type isabelle.Url to avoid oddities of java.net.URL (e.g. its "equals" method);
11 months ago, by wenzelm
unused;
11 months ago, by wenzelm
enforce rebuild of Isabelle/Scala + Isabelle/ML;
12 months ago, by wenzelm
updated to postgresql-42.7.1;
12 months ago, by wenzelm
updated to sqlite-jdbc-3.45.0.0, including slf4j-1.7.36;
12 months ago, by wenzelm
update to llncs-2.23;
12 months ago, by wenzelm
clarified bootstrap;
12 months ago, by wenzelm
clarified directories;
12 months ago, by wenzelm
clarified directories;
12 months ago, by wenzelm
obsolete (see also fc88b943e1b2);
12 months ago, by wenzelm
proper output, following 2cd23d587db9;
12 months ago, by wenzelm
always use patchelf on Linux: base-line is Ubuntu 18.04 where that works properly (see also e79294c4230c);
12 months ago, by wenzelm
clarified directories;
12 months ago, by wenzelm
more accurate Isabelle versions;
12 months ago, by wenzelm
more accurate Ubuntu versions;
12 months ago, by wenzelm
more uses of define_time_fun
12 months ago, by nipkow
translation to time functions now with canonical let.
12 months ago, by nipkow
merged
12 months ago, by paulson
A few new results (mostly brought in from other developments)
12 months ago, by paulson
merged
12 months ago, by nipkow
Added time function automation
12 months ago, by nipkow
streamlined type class specification
12 months ago, by haftmann
consolidated lemma name
12 months ago, by haftmann
support Phabricator on Ubuntu 22.04 LTS with PHP 8.1, using community form we.phorge.it version "2023 week 49";
12 months ago, by wenzelm
merged
12 months ago, by wenzelm
tuned;
12 months ago, by wenzelm
update links;
12 months ago, by wenzelm
follow post-maintenance updates of original Phabricator, as base-line for Phorge;
12 months ago, by wenzelm
refer to "localhost" as pro-forma domain;
12 months ago, by wenzelm
simplified specification of type class
12 months ago, by haftmann
consolidated name of lemma analogously to nat/int/word_bit_induct
12 months ago, by haftmann
more accurate syntax: 'obtain' vars are optional;
12 months ago, by wenzelm
clarified order, disregard structure of proof;
12 months ago, by wenzelm
minor performance tuning;
12 months ago, by wenzelm
tuned;
12 months ago, by wenzelm
more thorough treatment of hidden type variables within zproof;
12 months ago, by wenzelm
more uniform treatment of "hyps" within zproof;
12 months ago, by wenzelm
clarified order: follow Thm.fold_terms;
12 months ago, by wenzelm
merged
12 months ago, by wenzelm
clarified signature;
12 months ago, by wenzelm
clarified signature;
12 months ago, by wenzelm
tuned signature;
12 months ago, by wenzelm
tuned;
12 months ago, by wenzelm
clarified test: no exception yet;
12 months ago, by wenzelm
tuned;
12 months ago, by wenzelm
tuned;
12 months ago, by wenzelm
tuned signature: more direct operations;
12 months ago, by wenzelm
clarified signature;
12 months ago, by wenzelm
clarified signature: more direct operations;
12 months ago, by wenzelm
tuned signature;
12 months ago, by wenzelm
tuned;
12 months ago, by wenzelm
minor performance tuning, for important special case where consts are already expanded (e.g. re-certification within proof procedure);
12 months ago, by wenzelm
tuned whitespace;
12 months ago, by wenzelm
more robust: certify types uniformly (see also 62b75508eb66);
12 months ago, by wenzelm
tuned;
12 months ago, by wenzelm
clarified signature;
12 months ago, by wenzelm
clarified signature: avoid redundant Term.maxidx_of_term;
12 months ago, by wenzelm
proper check of result from Soft_Type_System.global_purge (amending b2bedb022a75);
12 months ago, by wenzelm
misc tuning and clarification: prefer Same.operation;
12 months ago, by wenzelm
clarified signature;
12 months ago, by wenzelm
tuned names;
12 months ago, by wenzelm
clarified signature;
12 months ago, by wenzelm
tuned whitespace;
12 months ago, by wenzelm
clarified modules;
12 months ago, by wenzelm
clarified signature;
12 months ago, by wenzelm
added and removed lemmas
12 months ago, by nipkow
proper SMTP session: set envelope sender address correctly;
12 months ago, by Fabian Huch
update javamail component with current jakarta mail APIs and eclipse angus implementation;
12 months ago, by Fabian Huch
tuned source structure;
12 months ago, by wenzelm
clarified signature;
12 months ago, by wenzelm
tuned;
12 months ago, by wenzelm
minor performance tuning;
12 months ago, by wenzelm
minor performance tuning;
12 months ago, by wenzelm
minor performance tuning;
12 months ago, by wenzelm
minor performance tuning;
12 months ago, by wenzelm
minor performance tuning;
12 months ago, by wenzelm
minor performance tuning;
12 months ago, by wenzelm
minor performance tuning;
12 months ago, by wenzelm
tuned;
12 months ago, by wenzelm
tuned signature;
12 months ago, by wenzelm
tuned signature;
12 months ago, by wenzelm
more zproofs, underlying Proofterm.unconstrain_thm_proof / Thm.unconstrainT;
12 months ago, by wenzelm
omit syntactic of_class check, which is in conflict with sort constraints within the logic;
12 months ago, by wenzelm
tuned;
12 months ago, by wenzelm
minor performance tuning;
12 months ago, by wenzelm
clarified signature;
12 months ago, by wenzelm
misc tuning and clarification;
12 months ago, by wenzelm
tuned signature;
12 months ago, by wenzelm
tuned signature: canonical argument order;
12 months ago, by wenzelm
tuned;
12 months ago, by wenzelm
clarified datatype ztyp: omit special case that rarely occurs (thanks to ZClass and ZClassp);
12 months ago, by wenzelm
clarified box_proof: use sort constraints within the logic;
12 months ago, by wenzelm
more operations (see also 8368160d3c65);
12 months ago, by wenzelm
proper support for complex types, not just type variables (amending 623789141e39);
12 months ago, by wenzelm
proper instantiation for make_const_proof, notably change of types for term variables;
12 months ago, by wenzelm
tuned names;
12 months ago, by wenzelm
more operations;
12 months ago, by wenzelm
clarified signature;
12 months ago, by wenzelm
minor performance tuning: proper Same.operation;
12 months ago, by wenzelm
minor performance tuning: proper Same.operation;
12 months ago, by wenzelm
tuned signature;
12 months ago, by wenzelm
minor performance tuning: proper Same.operation;
12 months ago, by wenzelm
minor performance tuning: proper Same.operation;
12 months ago, by wenzelm
tuned signature;
12 months ago, by wenzelm
tuned;
12 months ago, by wenzelm
pro-forma support for ZTerm.sorts_zproof;
12 months ago, by wenzelm
tuned comments;
12 months ago, by wenzelm
tuned structure;
12 months ago, by wenzelm
minor performance tuning: proper Same.operation;
12 months ago, by wenzelm
tuned names (again);
12 months ago, by wenzelm
clarified modules;
12 months ago, by wenzelm
clarified signature: more operations;
12 months ago, by wenzelm
tuned names;
12 months ago, by wenzelm
clarified signature;
12 months ago, by wenzelm
tuned;
12 months ago, by wenzelm
tuned whitespace;
12 months ago, by wenzelm
clarified signature;
12 months ago, by wenzelm
tuned;
12 months ago, by wenzelm
tuned;
12 months ago, by wenzelm
clarified signature: prefer Same.operation;
12 months ago, by wenzelm
tuned;
12 months ago, by wenzelm
more zproofs;
12 months ago, by wenzelm
more operations;
12 months ago, by wenzelm
clarified modules;
12 months ago, by wenzelm
minor performance tuning, following 703201dbd413;
12 months ago, by wenzelm
tuned;
12 months ago, by wenzelm
clarified signature: suppress unused fields;
12 months ago, by wenzelm
eliminate clone (amending e7796c55d840);
12 months ago, by wenzelm
minor performance tuning;
12 months ago, by wenzelm
more operations;
12 months ago, by wenzelm
more operations;
12 months ago, by wenzelm
tuned;
12 months ago, by wenzelm
clarified store_proof: before attributes are applied, to ensure proper thm_proof boxes for declaration attributes;
12 months ago, by wenzelm
tuned;
12 months ago, by wenzelm
tuned signature;
12 months ago, by wenzelm
tuned;
12 months ago, by wenzelm
tuned;
12 months ago, by wenzelm
more accurate Global_Theory.name_facts: burrow into expression of attributed theorems;
12 months ago, by wenzelm
clarified modules;
12 months ago, by wenzelm
clarified signature;
12 months ago, by wenzelm
tuned;
12 months ago, by wenzelm
clarified Global_Theory.store_proofs vs. Generic_Target.thm_definition / Attrib.global_notes;
12 months ago, by wenzelm
clarified signature;
12 months ago, by wenzelm
tuned;
12 months ago, by wenzelm
tuned: avoid duplicates;
12 months ago, by wenzelm
more operations;
12 months ago, by wenzelm
proper Thm.transfer;
12 months ago, by wenzelm
proper Thm.trim_context;
12 months ago, by wenzelm
clarified stored data: actual thm allows to replay zproofs in a modular manner;
12 months ago, by wenzelm
tuned signature;
12 months ago, by wenzelm
tuned signature, following Proofterm.thm_header;
12 months ago, by wenzelm
more robust: avoid crash of Thm.solve_constraints due to changed background theory, e.g. relevant for AFP/Transition_Systems_and_Automata;
12 months ago, by wenzelm
clarified signature;
12 months ago, by wenzelm
proper Thm_Name.make_list for thm_definition;
12 months ago, by wenzelm
more robust: avoid crash of AFP/Transition_Systems_and_Automata (amending fe4bd39bfeac and 43d8385db923);
12 months ago, by wenzelm
more robust: zproofs need to be enabled (amending 43d8385db923);
12 months ago, by wenzelm
more thorough thm definition via Global_Theory.register_proofs: store (and purge) zproofs;
12 months ago, by wenzelm
tuned names;
12 months ago, by wenzelm
clarified signature: support update of local_theory;
12 months ago, by wenzelm
tuned;
12 months ago, by wenzelm
clarified modules;
12 months ago, by wenzelm
tuned;
12 months ago, by wenzelm
unused;
12 months ago, by wenzelm
clarified modules;
12 months ago, by wenzelm
tuned;
12 months ago, by wenzelm
clarified modules;
12 months ago, by wenzelm
tuned;
12 months ago, by wenzelm
tuned signature;
12 months ago, by wenzelm
tuned;
12 months ago, by wenzelm
more operations;
12 months ago, by wenzelm
eliminate duplicate (see also 6cbcfac5b72e and af7b79271364);
12 months ago, by wenzelm
minor performance tuning: shorter names;
12 months ago, by wenzelm
minor performance tuning: static vs. dynamic rules;
12 months ago, by wenzelm
minor performance tuning;
12 months ago, by wenzelm
clarified signature: downgrade old-style Global_Theory.add_defs to Global_Theory.add_def without attributes;
12 months ago, by wenzelm
clarified signature;
12 months ago, by wenzelm
tuned;
12 months ago, by wenzelm
more thorough treatment of zproof vs. proof: avoid accidental storage of large structures;
12 months ago, by wenzelm
clarified signature;
12 months ago, by wenzelm
observe option "prune_proofs";
12 months ago, by wenzelm
clarified zproof storage: per-theory table in anticipation of session exports;
13 months ago, by wenzelm
proper thm_name for stored zproof;
13 months ago, by wenzelm
uniform treatment of lazy facts: actual proof terms are always strict;
13 months ago, by wenzelm
tuned;
13 months ago, by wenzelm
tuned whitespace;
13 months ago, by wenzelm
tuned;
13 months ago, by wenzelm
proper Thm.transfer;
13 months ago, by wenzelm
clarified context: avoid capture of thy2 within closure;
13 months ago, by wenzelm
tuned names;
13 months ago, by wenzelm
more informative exceptions;
13 months ago, by wenzelm
more permissive: allow collapse of term variables for equal results, e.g. relevant for metis (line 1882 of "~~/src/HOL/List.thy");
13 months ago, by wenzelm
tuned;
13 months ago, by wenzelm
more informative exception;
13 months ago, by wenzelm
clarified signature;
13 months ago, by wenzelm
clarified ML toplevel output: avoid "??." prefix;
13 months ago, by wenzelm
tuned;
13 months ago, by wenzelm
merged
13 months ago, by wenzelm
use strict Global_Theory.register_proofs as checkpoint for stored zproof, and thus reduce current zboxes;
13 months ago, by wenzelm
clarified signature;
13 months ago, by wenzelm
omit pointless future: proof terms are built sequentially;
13 months ago, by wenzelm
omit unclear / inaccurate renaming;
13 months ago, by wenzelm
more normalization: re-use Thm.solve_constraints as important checkpoint for results, notably Global_Theory.name_thm;
13 months ago, by wenzelm
more robust: avoid assumption about Context.certificate_theory;
13 months ago, by wenzelm
tuned;
13 months ago, by wenzelm
clarified pro-forma proof: no zboxes here (partially revert 686b7b14d041);
13 months ago, by wenzelm
tuned;
13 months ago, by wenzelm
tuned;
13 months ago, by wenzelm
more normalization;
13 months ago, by wenzelm
less ambitious normalization: term abstractions over terms and proofs, but not proofs over proofs (which may be large);
13 months ago, by wenzelm
tuned;
13 months ago, by wenzelm
more thorough beta contraction, following Envir.norm_term;
13 months ago, by wenzelm
tuned, following Envir.norm_term;
13 months ago, by wenzelm
more operations;
13 months ago, by wenzelm
merged
13 months ago, by nipkow
unused lemma
13 months ago, by nipkow
restore benchmark requirement heaps properly;
13 months ago, by Fabian Huch
continue build while waiting for updated schedule;
13 months ago, by Fabian Huch
clarified signature;
13 months ago, by Fabian Huch
added start-up sequence for benchmark with requirements;
13 months ago, by Fabian Huch
use single-threaded session build as benchmark (using ZF-Constructible);
13 months ago, by Fabian Huch
separate build processes for scheduler and scheduled;
13 months ago, by Fabian Huch
add delay and limit options for when schedule is considered outdated;
13 months ago, by Fabian Huch
proper closing order;
13 months ago, by Fabian Huch
read serial for schedules (amending 2039f360);
13 months ago, by Fabian Huch
more thorough beta contraction;
13 months ago, by wenzelm
tuned whitespace;
13 months ago, by wenzelm
tuned;
13 months ago, by wenzelm
more operations, following proofterm.ML;
13 months ago, by wenzelm
tuned;
13 months ago, by wenzelm
clarified signature, following Term.subst_bounds_same;
13 months ago, by wenzelm
tuned whitespace;
13 months ago, by wenzelm
minor performance tuning: more concise union;
13 months ago, by wenzelm
tuned comments;
13 months ago, by wenzelm
tuned, following close_proof;
13 months ago, by wenzelm
proper treatment of proof hyps, following 8368160d3c65;
13 months ago, by wenzelm
proper treatment of proof hyps: unchangeable, like bound;
13 months ago, by wenzelm
proper Thm.transfer (required for zproofs);
13 months ago, by wenzelm
clarified signature;
13 months ago, by wenzelm
proper beta_norm after instantiation (amending 90c5aadcc4b2);
13 months ago, by wenzelm
minor performance tuning: more direct beta_norm;
13 months ago, by wenzelm
more robust norm_proof: turn env into instantiation, based on visible statement;
13 months ago, by wenzelm
proper scope of cache (amending 61af3e917597);
13 months ago, by wenzelm
tuned comments;
13 months ago, by wenzelm
tuned names;
13 months ago, by wenzelm
tuned signature;
13 months ago, by wenzelm
more zproofs;
13 months ago, by wenzelm
more operations: zterm ordering that follows fast_term_ord;
13 months ago, by wenzelm
clarified signature;
13 months ago, by wenzelm
clarified modules;
13 months ago, by wenzelm
more zproofs;
13 months ago, by wenzelm
more zproofs, imitating existing proofs (which are a bit rough here);
13 months ago, by wenzelm
tuned signature;
13 months ago, by wenzelm
tuned whitespace;
13 months ago, by wenzelm
minor performance tuning;
13 months ago, by wenzelm
tuned comments (see also 476a239d3e0e and possibly 4b62e0cb3aa8);
13 months ago, by wenzelm
merged
13 months ago, by wenzelm
minor performance tuning;
13 months ago, by wenzelm
tuned;
13 months ago, by wenzelm
minor performance tuning: prefer Same.operation;
13 months ago, by wenzelm
clarified signature;
13 months ago, by wenzelm
minor performance tuning;
13 months ago, by wenzelm
more operations;
13 months ago, by wenzelm
revert 17fda85a33dc: renaming is not necessarily unique, e.g. [("x", "x"), ("x", "y")];
13 months ago, by wenzelm
misc tuning and clarification;
13 months ago, by wenzelm
minor performance tuning: prefer Symset.T;
13 months ago, by wenzelm
minor performace tuning;
13 months ago, by wenzelm
minor performance tuning: prefer Same.operation;
13 months ago, by wenzelm
tuned: more standard accumulation;
13 months ago, by wenzelm
tuned;
13 months ago, by wenzelm
clarified modules;
13 months ago, by wenzelm
clarified signature;
13 months ago, by wenzelm
tuned whitespace;
13 months ago, by wenzelm
tuned;
13 months ago, by wenzelm
proper ZTerm.lift_proof (amending 4a1a25bdf81d);
13 months ago, by wenzelm
filter predecessors properly (amending ee405c40db72);
13 months ago, by Fabian Huch
improve graphical clarity by omitting intra-host dependencies (following ee405c40db72);
13 months ago, by Fabian Huch
more zproofs;
13 months ago, by wenzelm
minor performance tuning: more direct abstraction level;
13 months ago, by wenzelm
more general Logic.incr_indexes_operation;
13 months ago, by wenzelm
tuned;
13 months ago, by wenzelm
tuned;
13 months ago, by wenzelm
clarified modules;
13 months ago, by wenzelm
clarified ML;
13 months ago, by wenzelm
clarified signature;
13 months ago, by wenzelm
tuned signature;
13 months ago, by wenzelm
avoid accidental capture of theory value, and thus reduce heap size again (amending 5109e4b2a292);
13 months ago, by wenzelm
tuned;
13 months ago, by wenzelm
more robust: proper Proofterm.get_proofs_level with bound check;
13 months ago, by wenzelm
tuned;
13 months ago, by wenzelm
clarified signature: fewer tuples;
13 months ago, by wenzelm
clarified signature: fewer tuples;
13 months ago, by wenzelm
clarified signature: more explicit get_proofs_level with bounds check;
13 months ago, by wenzelm
merged
13 months ago, by wenzelm
misc tuning and clarification: more standard Same.commit discipline;
13 months ago, by wenzelm
tuned;
13 months ago, by wenzelm
tuned names;
13 months ago, by wenzelm
more operations;
13 months ago, by wenzelm
minor performance tuning: more careful treatment of empty environment;
13 months ago, by wenzelm
clarified signature;
13 months ago, by wenzelm
more zproofs;
13 months ago, by wenzelm
clarified signature: support shared cache;
13 months ago, by wenzelm
tuned;
13 months ago, by wenzelm
tuned: avoid shadowing;
13 months ago, by wenzelm
more zproofs;
13 months ago, by wenzelm
tuned;
13 months ago, by wenzelm
more operations;
13 months ago, by wenzelm
tuned signature;
13 months ago, by wenzelm
tuned names;
13 months ago, by wenzelm
tuned -- eliminate clones;
13 months ago, by wenzelm
tuned;
13 months ago, by wenzelm
more operations;
13 months ago, by wenzelm
more operations;
13 months ago, by wenzelm
tuned;
13 months ago, by wenzelm
clarified signature;
13 months ago, by wenzelm
tuned;
13 months ago, by wenzelm
tuned;
13 months ago, by wenzelm
consider schedule calculation time in estimation;
13 months ago, by Fabian Huch
compare previous build schedule with new one, to prevent regressions;
13 months ago, by Fabian Huch
clarified: build schedules may be outdated when empty, after some time, or due to build progress;
13 months ago, by Fabian Huch
store previous build jobs in graph so schedules can be used later in the build process;
13 months ago, by Fabian Huch
add serial for build schedule to avoid unnecessary db read/writes;
13 months ago, by Fabian Huch
tuned;
13 months ago, by Fabian Huch
clarified;
13 months ago, by Fabian Huch
tuned;
13 months ago, by Fabian Huch
use build database to synchronize build schedule computed on master node (e.g., such that view on cluster is consistent);
13 months ago, by Fabian Huch
add build uuid to schedule;
13 months ago, by Fabian Huch
tuned;
13 months ago, by Fabian Huch
use schedule directly instead of extra cache;
13 months ago, by Fabian Huch
added build schedule command-line wrapper;
13 months ago, by Fabian Huch
added graphical representation of build schedules;
13 months ago, by Fabian Huch
clarified build heuristics parameters;
13 months ago, by Fabian Huch
proper parallel paths: factor in elapsed time;
13 months ago, by Fabian Huch
performance tuning: cache estimates;
13 months ago, by Fabian Huch
misc tuning and clarification;
13 months ago, by wenzelm
tuned;
13 months ago, by wenzelm
misc tuning and clarification, following Term.incr_bv / Term.incr_boundvars;
13 months ago, by wenzelm
tuned;
13 months ago, by wenzelm
tuned;
13 months ago, by wenzelm
minor performance tuning: regular Same.operation;
13 months ago, by wenzelm
clarified signature: more standard argument order;
13 months ago, by wenzelm
clarified signature: more standard argument order;
13 months ago, by wenzelm
tuned whitespace;
13 months ago, by wenzelm
tuned: more standard names;
13 months ago, by wenzelm
clarified signature;
13 months ago, by wenzelm
tuned: prefer Same.commit;
13 months ago, by wenzelm
tuned: more standard argument order;
13 months ago, by wenzelm
clarified signature;
13 months ago, by wenzelm
more operations;
13 months ago, by wenzelm
tuned comments;
13 months ago, by wenzelm
tuned structure;
13 months ago, by wenzelm
tuned;
13 months ago, by wenzelm
merged
13 months ago, by wenzelm
performance tuning: cache for ztyp_of within zterm_of;
13 months ago, by wenzelm
tuned names;
13 months ago, by wenzelm
minor performance tuning;
13 months ago, by wenzelm
more zproofs;
13 months ago, by wenzelm
minor performance tuning;
13 months ago, by wenzelm
tuned;
13 months ago, by wenzelm
more zproofs;
13 months ago, by wenzelm
clarified modules;
13 months ago, by wenzelm
more zproofs;
13 months ago, by wenzelm
more zproofs;
13 months ago, by wenzelm
proper treatment of ZConstP: term represents body of closure;
13 months ago, by wenzelm
proper substitution of types within term;
13 months ago, by wenzelm
more accurate treatment of term variables after instantiation of type variables;
13 months ago, by wenzelm
tuned signature;
13 months ago, by wenzelm
tuned;
13 months ago, by wenzelm
check that Isar proofs contain one 'show'
13 months ago, by blanchet
include unnamed chained facts in Sledgehammer's relevance filter
13 months ago, by blanchet
merge
13 months ago, by blanchet
removed hack in Sledgehammer that confuses preplay and gives Sledgehammer a strange semantics
13 months ago, by blanchet
don't freeze terms in Sledgehammer, as this has a bad impact on 'using' facts
13 months ago, by blanchet
tuned T functions: now 0 if not recursive
13 months ago, by nipkow
minor performance tuning;
13 months ago, by wenzelm
tuned;
13 months ago, by wenzelm
more zproofs;
13 months ago, by wenzelm
misc tuning and clarification;
13 months ago, by wenzelm
more zproofs;
13 months ago, by wenzelm
more operations;
13 months ago, by wenzelm
more operations;
13 months ago, by wenzelm
tuned;
13 months ago, by wenzelm
clarified signature;
13 months ago, by wenzelm
more zproofs;
13 months ago, by wenzelm
more ML pretty-printing;
13 months ago, by wenzelm
clarified const_proof vs. zproof_name;
13 months ago, by wenzelm
merged
13 months ago, by wenzelm
more zproofs;
13 months ago, by wenzelm
less
more
|
(0)
-30000
-10000
-3000
-1000
-480
+480
+1000
tip