Mercurial
Mercurial
>
repos
>
isabelle
/ graph
summary
|
shortlog
|
changelog
| graph |
tags
|
bookmarks
|
branches
|
files
|
gz
|
help
less
more
|
(0)
-30000
-10000
-3000
-1000
-240
+240
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.
more robust (amending 1600fb749c54), to support the following corner case:
3 months ago, by wenzelm
proper test options;
3 months ago, by wenzelm
proper history_base for linux_arm;
3 months ago, by wenzelm
updated to PostgreSQL 12 on Ubuntu 20.04;
3 months ago, by wenzelm
routine build + test for linux_arm;
3 months ago, by wenzelm
disable test on "augsburg1": machine will be dismantled;
3 months ago, by wenzelm
add approximation factors in build schedule to estimate build times more conservatively;
3 months ago, by Fabian Huch
merged
3 months ago, by paulson
Type class patch suggested by Achim Brucker, plus tidied lemma
3 months ago, by paulson
rearranged and reformulated abstract classes for bit structures and operations
3 months ago, by haftmann
Three new lemmas
3 months ago, by paulson
tuned proof: avoid z3 to make it work on arm64-linux;
3 months ago, by wenzelm
update to jdk-21.0.2;
3 months ago, by wenzelm
make build process state protected to avoid copying in subclasses (e.g. for database connections);
3 months ago, by Fabian Huch
add build_sync tag to sync certain options (e.g., build_engine) across build processes;
3 months ago, by Fabian Huch
clarified Mercurial version: presumably the last version that supports both python2 and python3;
3 months ago, by wenzelm
more robust: avoid crash on non-Linux systems;
3 months ago, by wenzelm
clarified webserver names;
3 months ago, by wenzelm
proper Apache.php_name;
3 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);
3 months ago, by wenzelm
tuned source structure;
3 months ago, by wenzelm
more robust systemd configuration;
3 months ago, by wenzelm
more robust nginx configuration, notably for "certbot --nginx -d DOMAIN";
3 months ago, by wenzelm
tuned whitespace in generated file;
3 months ago, by wenzelm
tuned;
3 months ago, by wenzelm
clarified modules;
3 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);
3 months ago, by wenzelm
proper php-fpm configuration for nginx;
3 months ago, by wenzelm
support multiple webservers: Apache or Nginx;
3 months ago, by wenzelm
tuned;
3 months ago, by wenzelm
clarified signature: explicit type isabelle.Url to avoid oddities of java.net.URL (e.g. its "equals" method);
3 months ago, by wenzelm
unused;
3 months ago, by wenzelm
enforce rebuild of Isabelle/Scala + Isabelle/ML;
3 months ago, by wenzelm
updated to postgresql-42.7.1;
3 months ago, by wenzelm
updated to sqlite-jdbc-3.45.0.0, including slf4j-1.7.36;
3 months ago, by wenzelm
update to llncs-2.23;
3 months ago, by wenzelm
clarified bootstrap;
3 months ago, by wenzelm
clarified directories;
3 months ago, by wenzelm
clarified directories;
3 months ago, by wenzelm
obsolete (see also fc88b943e1b2);
3 months ago, by wenzelm
proper output, following 2cd23d587db9;
3 months ago, by wenzelm
always use patchelf on Linux: base-line is Ubuntu 18.04 where that works properly (see also e79294c4230c);
3 months ago, by wenzelm
clarified directories;
3 months ago, by wenzelm
more accurate Isabelle versions;
3 months ago, by wenzelm
more accurate Ubuntu versions;
3 months ago, by wenzelm
more uses of define_time_fun
3 months ago, by nipkow
translation to time functions now with canonical let.
3 months ago, by nipkow
merged
4 months ago, by paulson
A few new results (mostly brought in from other developments)
4 months ago, by paulson
merged
4 months ago, by nipkow
Added time function automation
4 months ago, by nipkow
streamlined type class specification
4 months ago, by haftmann
consolidated lemma name
4 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";
4 months ago, by wenzelm
merged
4 months ago, by wenzelm
tuned;
4 months ago, by wenzelm
update links;
4 months ago, by wenzelm
follow post-maintenance updates of original Phabricator, as base-line for Phorge;
4 months ago, by wenzelm
refer to "localhost" as pro-forma domain;
4 months ago, by wenzelm
simplified specification of type class
4 months ago, by haftmann
consolidated name of lemma analogously to nat/int/word_bit_induct
4 months ago, by haftmann
more accurate syntax: 'obtain' vars are optional;
4 months ago, by wenzelm
clarified order, disregard structure of proof;
4 months ago, by wenzelm
minor performance tuning;
4 months ago, by wenzelm
tuned;
4 months ago, by wenzelm
more thorough treatment of hidden type variables within zproof;
4 months ago, by wenzelm
more uniform treatment of "hyps" within zproof;
4 months ago, by wenzelm
clarified order: follow Thm.fold_terms;
4 months ago, by wenzelm
merged
4 months ago, by wenzelm
clarified signature;
4 months ago, by wenzelm
clarified signature;
4 months ago, by wenzelm
tuned signature;
4 months ago, by wenzelm
tuned;
4 months ago, by wenzelm
clarified test: no exception yet;
4 months ago, by wenzelm
tuned;
4 months ago, by wenzelm
tuned;
4 months ago, by wenzelm
tuned signature: more direct operations;
4 months ago, by wenzelm
clarified signature;
4 months ago, by wenzelm
clarified signature: more direct operations;
4 months ago, by wenzelm
tuned signature;
4 months ago, by wenzelm
tuned;
4 months ago, by wenzelm
minor performance tuning, for important special case where consts are already expanded (e.g. re-certification within proof procedure);
4 months ago, by wenzelm
tuned whitespace;
4 months ago, by wenzelm
more robust: certify types uniformly (see also 62b75508eb66);
4 months ago, by wenzelm
tuned;
4 months ago, by wenzelm
clarified signature;
4 months ago, by wenzelm
clarified signature: avoid redundant Term.maxidx_of_term;
4 months ago, by wenzelm
proper check of result from Soft_Type_System.global_purge (amending b2bedb022a75);
4 months ago, by wenzelm
misc tuning and clarification: prefer Same.operation;
4 months ago, by wenzelm
clarified signature;
4 months ago, by wenzelm
tuned names;
4 months ago, by wenzelm
clarified signature;
4 months ago, by wenzelm
tuned whitespace;
4 months ago, by wenzelm
clarified modules;
4 months ago, by wenzelm
clarified signature;
4 months ago, by wenzelm
added and removed lemmas
4 months ago, by nipkow
proper SMTP session: set envelope sender address correctly;
4 months ago, by Fabian Huch
update javamail component with current jakarta mail APIs and eclipse angus implementation;
4 months ago, by Fabian Huch
tuned source structure;
4 months ago, by wenzelm
clarified signature;
4 months ago, by wenzelm
tuned;
4 months ago, by wenzelm
minor performance tuning;
4 months ago, by wenzelm
minor performance tuning;
4 months ago, by wenzelm
minor performance tuning;
4 months ago, by wenzelm
minor performance tuning;
4 months ago, by wenzelm
minor performance tuning;
4 months ago, by wenzelm
minor performance tuning;
4 months ago, by wenzelm
minor performance tuning;
4 months ago, by wenzelm
tuned;
4 months ago, by wenzelm
tuned signature;
4 months ago, by wenzelm
tuned signature;
4 months ago, by wenzelm
more zproofs, underlying Proofterm.unconstrain_thm_proof / Thm.unconstrainT;
4 months ago, by wenzelm
omit syntactic of_class check, which is in conflict with sort constraints within the logic;
4 months ago, by wenzelm
tuned;
4 months ago, by wenzelm
minor performance tuning;
4 months ago, by wenzelm
clarified signature;
4 months ago, by wenzelm
misc tuning and clarification;
4 months ago, by wenzelm
tuned signature;
4 months ago, by wenzelm
tuned signature: canonical argument order;
4 months ago, by wenzelm
tuned;
4 months ago, by wenzelm
clarified datatype ztyp: omit special case that rarely occurs (thanks to ZClass and ZClassp);
4 months ago, by wenzelm
clarified box_proof: use sort constraints within the logic;
4 months ago, by wenzelm
more operations (see also 8368160d3c65);
4 months ago, by wenzelm
proper support for complex types, not just type variables (amending 623789141e39);
4 months ago, by wenzelm
proper instantiation for make_const_proof, notably change of types for term variables;
4 months ago, by wenzelm
tuned names;
4 months ago, by wenzelm
more operations;
4 months ago, by wenzelm
clarified signature;
4 months ago, by wenzelm
minor performance tuning: proper Same.operation;
4 months ago, by wenzelm
minor performance tuning: proper Same.operation;
4 months ago, by wenzelm
tuned signature;
4 months ago, by wenzelm
minor performance tuning: proper Same.operation;
4 months ago, by wenzelm
minor performance tuning: proper Same.operation;
4 months ago, by wenzelm
tuned signature;
4 months ago, by wenzelm
tuned;
4 months ago, by wenzelm
pro-forma support for ZTerm.sorts_zproof;
4 months ago, by wenzelm
tuned comments;
4 months ago, by wenzelm
tuned structure;
4 months ago, by wenzelm
minor performance tuning: proper Same.operation;
4 months ago, by wenzelm
tuned names (again);
4 months ago, by wenzelm
clarified modules;
4 months ago, by wenzelm
clarified signature: more operations;
4 months ago, by wenzelm
tuned names;
4 months ago, by wenzelm
clarified signature;
4 months ago, by wenzelm
tuned;
4 months ago, by wenzelm
tuned whitespace;
4 months ago, by wenzelm
clarified signature;
4 months ago, by wenzelm
tuned;
4 months ago, by wenzelm
tuned;
4 months ago, by wenzelm
clarified signature: prefer Same.operation;
4 months ago, by wenzelm
tuned;
4 months ago, by wenzelm
more zproofs;
4 months ago, by wenzelm
more operations;
4 months ago, by wenzelm
clarified modules;
4 months ago, by wenzelm
minor performance tuning, following 703201dbd413;
4 months ago, by wenzelm
tuned;
4 months ago, by wenzelm
clarified signature: suppress unused fields;
4 months ago, by wenzelm
eliminate clone (amending e7796c55d840);
4 months ago, by wenzelm
minor performance tuning;
4 months ago, by wenzelm
more operations;
4 months ago, by wenzelm
more operations;
4 months ago, by wenzelm
tuned;
4 months ago, by wenzelm
clarified store_proof: before attributes are applied, to ensure proper thm_proof boxes for declaration attributes;
4 months ago, by wenzelm
tuned;
4 months ago, by wenzelm
tuned signature;
4 months ago, by wenzelm
tuned;
4 months ago, by wenzelm
tuned;
4 months ago, by wenzelm
more accurate Global_Theory.name_facts: burrow into expression of attributed theorems;
4 months ago, by wenzelm
clarified modules;
4 months ago, by wenzelm
clarified signature;
4 months ago, by wenzelm
tuned;
4 months ago, by wenzelm
clarified Global_Theory.store_proofs vs. Generic_Target.thm_definition / Attrib.global_notes;
4 months ago, by wenzelm
clarified signature;
4 months ago, by wenzelm
tuned;
4 months ago, by wenzelm
tuned: avoid duplicates;
4 months ago, by wenzelm
more operations;
4 months ago, by wenzelm
proper Thm.transfer;
4 months ago, by wenzelm
proper Thm.trim_context;
4 months ago, by wenzelm
clarified stored data: actual thm allows to replay zproofs in a modular manner;
4 months ago, by wenzelm
tuned signature;
4 months ago, by wenzelm
tuned signature, following Proofterm.thm_header;
4 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;
4 months ago, by wenzelm
clarified signature;
4 months ago, by wenzelm
proper Thm_Name.make_list for thm_definition;
4 months ago, by wenzelm
more robust: avoid crash of AFP/Transition_Systems_and_Automata (amending fe4bd39bfeac and 43d8385db923);
4 months ago, by wenzelm
more robust: zproofs need to be enabled (amending 43d8385db923);
4 months ago, by wenzelm
more thorough thm definition via Global_Theory.register_proofs: store (and purge) zproofs;
4 months ago, by wenzelm
tuned names;
4 months ago, by wenzelm
clarified signature: support update of local_theory;
4 months ago, by wenzelm
tuned;
4 months ago, by wenzelm
clarified modules;
4 months ago, by wenzelm
tuned;
4 months ago, by wenzelm
unused;
4 months ago, by wenzelm
clarified modules;
4 months ago, by wenzelm
tuned;
4 months ago, by wenzelm
clarified modules;
4 months ago, by wenzelm
tuned;
4 months ago, by wenzelm
tuned signature;
4 months ago, by wenzelm
tuned;
4 months ago, by wenzelm
more operations;
4 months ago, by wenzelm
eliminate duplicate (see also 6cbcfac5b72e and af7b79271364);
4 months ago, by wenzelm
minor performance tuning: shorter names;
4 months ago, by wenzelm
minor performance tuning: static vs. dynamic rules;
4 months ago, by wenzelm
minor performance tuning;
4 months ago, by wenzelm
clarified signature: downgrade old-style Global_Theory.add_defs to Global_Theory.add_def without attributes;
4 months ago, by wenzelm
clarified signature;
4 months ago, by wenzelm
tuned;
4 months ago, by wenzelm
more thorough treatment of zproof vs. proof: avoid accidental storage of large structures;
4 months ago, by wenzelm
clarified signature;
4 months ago, by wenzelm
observe option "prune_proofs";
4 months ago, by wenzelm
clarified zproof storage: per-theory table in anticipation of session exports;
4 months ago, by wenzelm
proper thm_name for stored zproof;
4 months ago, by wenzelm
uniform treatment of lazy facts: actual proof terms are always strict;
4 months ago, by wenzelm
tuned;
4 months ago, by wenzelm
tuned whitespace;
4 months ago, by wenzelm
tuned;
4 months ago, by wenzelm
proper Thm.transfer;
4 months ago, by wenzelm
clarified context: avoid capture of thy2 within closure;
4 months ago, by wenzelm
tuned names;
4 months ago, by wenzelm
more informative exceptions;
4 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");
4 months ago, by wenzelm
tuned;
4 months ago, by wenzelm
more informative exception;
4 months ago, by wenzelm
clarified signature;
4 months ago, by wenzelm
clarified ML toplevel output: avoid "??." prefix;
4 months ago, by wenzelm
tuned;
4 months ago, by wenzelm
merged
4 months ago, by wenzelm
use strict Global_Theory.register_proofs as checkpoint for stored zproof, and thus reduce current zboxes;
4 months ago, by wenzelm
clarified signature;
4 months ago, by wenzelm
omit pointless future: proof terms are built sequentially;
4 months ago, by wenzelm
omit unclear / inaccurate renaming;
4 months ago, by wenzelm
more normalization: re-use Thm.solve_constraints as important checkpoint for results, notably Global_Theory.name_thm;
4 months ago, by wenzelm
more robust: avoid assumption about Context.certificate_theory;
4 months ago, by wenzelm
tuned;
4 months ago, by wenzelm
clarified pro-forma proof: no zboxes here (partially revert 686b7b14d041);
4 months ago, by wenzelm
tuned;
4 months ago, by wenzelm
tuned;
4 months ago, by wenzelm
more normalization;
4 months ago, by wenzelm
less ambitious normalization: term abstractions over terms and proofs, but not proofs over proofs (which may be large);
4 months ago, by wenzelm
tuned;
4 months ago, by wenzelm
less
more
|
(0)
-30000
-10000
-3000
-1000
-240
+240
tip