isabelle: Graph

merged
5 days ago, by haftmann
modernized and streamlined theory
5 days ago, by haftmann
provide somewhat incomplete naproche-20250125 for testing;
5 days ago, by wenzelm
conservative update to stackage lts-22.15 and ghc-9.6.6;
5 days ago, by wenzelm
conservative update to stack-2.15.7;
5 days ago, by wenzelm
merged
6 days ago, by paulson
merged
6 days ago, by paulson
Tidying more old proofs
6 days ago, by paulson
discontinue old Java 17 LTS;
6 days ago, by wenzelm
update versions for release -- one behind current jedit-5.7.0;
6 days ago, by wenzelm
more explicit system dependencies;
6 days ago, by wenzelm
proper executable from "isabelle ocaml_opam env";
6 days ago, by wenzelm
update to postgresql-42.7.5;
6 days ago, by wenzelm
update to jdk-21.0.6;
6 days ago, by wenzelm
update for release;
7 days ago, by wenzelm
misc tuning for release;
7 days ago, by wenzelm
more NEWS;
7 days ago, by wenzelm
more authors;
7 days ago, by wenzelm
merged
7 days ago, by wenzelm
tuned names: follow HOL Light;
7 days ago, by wenzelm
more antiquotations;
7 days ago, by wenzelm
support for @{instantiate (no_beta) ...};
7 days ago, by wenzelm
minor performance tuning: more fine-grained guard to skip irrelevant items;
7 days ago, by wenzelm
proper treatment of variables with the same name, but different sorts/types: this routinely happens in HOL Light (see also 0e2f019477e2), as well as theory "HOL-Algebra.Algebraic_Closure_Type" (line 77);
7 days ago, by wenzelm
tuned output;
7 days ago, by wenzelm
minor performance tuning: omit redundant inst_cterm;
8 days ago, by wenzelm
tuned signature: more operations;
8 days ago, by wenzelm
misc tuning: more concise operations on prems (without change of exceptions);
8 days ago, by wenzelm
tuned: prefer Thm.prem_of, which differes wrt. exceptions that are not handled here;
8 days ago, by wenzelm
tuned signature: more explicit operations;
8 days ago, by wenzelm
tuned: more direct Thm.cprem_of;
8 days ago, by wenzelm
misc tuning;
9 days ago, by wenzelm
tuned names;
9 days ago, by wenzelm
more direct emulation of HOL Light inferences: prefer Pure rules over HOL thms;
9 days ago, by wenzelm
tuned;
9 days ago, by wenzelm
misc tuning: prefer specific variants of Thm.dest_comb;
9 days ago, by wenzelm
more robust: explicit check for "Trueprop";
9 days ago, by wenzelm
tuned;
9 days ago, by wenzelm
more robust: explicit check for "Trueprop";
9 days ago, by wenzelm
clarified signature: more uniform cterm operations, without context;
9 days ago, by wenzelm
tuned;
9 days ago, by wenzelm
tuned;
9 days ago, by wenzelm
misc tuning: more antiquotations;
10 days ago, by wenzelm
clarified exceptions;
9 days ago, by wenzelm
tuned names, following HOL Light sources;
10 days ago, by wenzelm
more robust alignments for HOL Light Release-3.0.0;
10 days ago, by wenzelm
provide num_Axiom for HOL Light Release-3.0.0;
10 days ago, by wenzelm
tuned proofs;
10 days ago, by wenzelm
more comments;
10 days ago, by wenzelm
cleanup generated bounds;
10 days ago, by wenzelm
discontinue special treatment of HOL Light CONJUNCTS: this is better done in Isabelle;
11 days ago, by wenzelm
clarified bundle names, in terms of the "offline" tool;
11 days ago, by wenzelm
proper result from "offline" tool;
11 days ago, by wenzelm
optional maps.lst;
11 days ago, by wenzelm
tuned output: proper progress;
11 days ago, by wenzelm
support tracing (with proper guard);
11 days ago, by wenzelm
more README;
11 days ago, by wenzelm
allow to load additional HOL Light files, after "hol.ml";
11 days ago, by wenzelm
more complete bundle;
12 days ago, by wenzelm
tuned README;
12 days ago, by wenzelm
proper settings;
12 days ago, by wenzelm
clarified compression;
12 days ago, by wenzelm
clarified patches: avoid duplication;
12 days ago, by wenzelm
clarified patches;
12 days ago, by wenzelm
more explicit stages, with timing messages;
12 days ago, by wenzelm
avoid redundant repository clone;
12 days ago, by wenzelm
move material from https://gitlab.inria.fr/hol-light-isabelle/hol-light 72b2b702eadb and https://gitlab.inria.fr/hol-light-isabelle/import ce58755b0232 into Isabelle repository: results from running "isabelle component_hol_light_import" of previous version;
12 days ago, by wenzelm
original HOL Light "offline" material by Cezary Kaliszyk and Alexander Krauss, from http://cl-informatik.uibk.ac.at/users/cek/import/holimport.tgz 27-Nov-2013 (37372 bytes);
12 days ago, by wenzelm
tuned names;
12 days ago, by wenzelm
misc cleanup and minor performance tuning;
12 days ago, by wenzelm
clarified signature;
13 days ago, by wenzelm
tuned: prefer existing operations;
13 days ago, by wenzelm
tuned source structure;
13 days ago, by wenzelm
tuned state operations;
13 days ago, by wenzelm
tuned signature;
13 days ago, by wenzelm
misc tuning and clarification: prefer state operations, avoid redundant ctyp_of/cterm_of;
13 days ago, by wenzelm
tuned;
13 days ago, by wenzelm
tuned;
13 days ago, by wenzelm
tuned proofs;
13 days ago, by wenzelm
merged
7 days ago, by Fabian Huch
update to javamail-20250122;
8 days ago, by Fabian Huch
merged
8 days ago, by paulson
more tidying
8 days ago, by paulson
tuned messages;
8 days ago, by Fabian Huch
clarified: more arguments;
9 days ago, by Fabian Huch
explicit error message when Solr database does not exist;
9 days ago, by Fabian Huch
copy instead of symlink managed Find_Facts indexes: portable, and allows updating with local sessions;
9 days ago, by Fabian Huch
clarified CLI arg vs. option;
9 days ago, by Fabian Huch
clarified;
9 days ago, by Fabian Huch
clarified find_facts URL;
9 days ago, by Fabian Huch
clarified CLI options: web dir only in $FIND_FACTS_HOME_USER/web;
9 days ago, by Fabian Huch
clarified settings: $FIND_FACTS_HOME_USER instead of individual directories;
9 days ago, by Fabian Huch
clarified: Find_Facts indexes instead of Solr components;
9 days ago, by Fabian Huch
clarified: application-specific $SOLR_DATA, e.g. $FIND_FACTS_SOLR_DATA;
9 days ago, by Fabian Huch
merged
10 days ago, by Fabian Huch
clarified: more operations;
10 days ago, by Fabian Huch
tuned default nightly start: less events at 00:17:00;
10 days ago, by Fabian Huch
use cycles in ci triggers;
10 days ago, by Fabian Huch
varying-length calendar cycles, e.g. for ci jobs every week on a certain day/time;
10 days ago, by Fabian Huch
clarified;
11 days ago, by Fabian Huch
tuned whitespace;
13 days ago, by Fabian Huch
add find_facts_index command to use within Isabelle/Scala;
2 weeks ago, by Fabian Huch
clarified: add afp_root argument;
2 weeks ago, by Fabian Huch
merged
10 days ago, by nipkow
introduced/overloaded power operator ^^ lists
10 days ago, by nipkow
systematic checks for bit operations and more rules on symbolic terms
10 days ago, by haftmann
explicitly report dependencies on missing code equations
10 days ago, by haftmann
simplified old proofs
11 days ago, by paulson
merged
13 days ago, by paulson
merged
13 days ago, by paulson
A variety of tweaks
13 days ago, by paulson
avoid legacy warnings in "test_code check in OCaml";
13 days ago, by wenzelm
proper condition for strict "test_code check in OCaml" and "test_code check in GHC";
13 days ago, by wenzelm
more NEWS;
13 days ago, by wenzelm
merged
13 days ago, by wenzelm
misc tuning;
13 days ago, by wenzelm
tuned;
13 days ago, by wenzelm
tuned;
13 days ago, by wenzelm
clarified pattern matching;
13 days ago, by wenzelm
misc tuning;
13 days ago, by wenzelm
misc tuning and clarification;
13 days ago, by wenzelm
tuned;
13 days ago, by wenzelm
clarified exceptions and messages: use "error" only for user-errors, not system failures;
13 days ago, by wenzelm
minor performance tuning: more elementary operations;
13 days ago, by wenzelm
minor performance tuning;
13 days ago, by wenzelm
clarified inst_type: more direct Thm.instantiate_frees;
13 days ago, by wenzelm
more direct Thm.free: avoid re-certification;
13 days ago, by wenzelm
clarified signature: more explicit types;
13 days ago, by wenzelm