isabelle: Graph

added offset to Mirabelle's tptp output names
2021-09-20, by desharna
tuned zipperposition config in sledgehammer
2021-10-04, by desharna
considered slices overhead in sledgehammer
2021-10-04, by desharna
tuned atp_prover sliding
2021-09-29, by desharna
tuned Zipperposition slides in sledgehammer
2021-09-29, by desharna
include arm64-linux;
2021-10-06, by wenzelm
updated to Vampire 4.6, as proposed by Martin Desharnais;
2021-10-06, by wenzelm
build from official downloads;
2021-10-06, by wenzelm
build just one vampire version;
2021-10-06, by wenzelm
clarified signature;
2021-10-06, by wenzelm
maintain previous theory identifier to support semantic caching, notably in Isabelle/Naproche;
2021-10-05, by wenzelm
more exports, notably for Isabelle/Naproche;
2021-10-05, by wenzelm
include arm64-linux;
2021-10-05, by wenzelm
prefer existing OCaml installation;
2021-10-05, by wenzelm
include arm64-linux;
2021-10-04, by wenzelm
no patchelf on macOS (undetected due to cached executables?);
2021-10-04, by wenzelm
provide opam-2.1.0 for experimentation;
2021-10-04, by wenzelm
rebuild cygwin-20211004.tar.gz;
2021-10-04, by wenzelm
include arm64-linux;
2021-10-04, by wenzelm
updated to cygwin-20211004: build again;
2021-10-04, by wenzelm
merged
2021-10-04, by wenzelm
removed pointless NEWS: both Docker/ubuntu and Cygwin provide perl by default;
2021-10-04, by wenzelm
actually use cygwin-20211002 (amending ff0ca375457c);
2021-10-04, by wenzelm
discontinued perl;
2021-10-04, by wenzelm
clarified signature;
2021-10-04, by wenzelm
proper term operation Term.dest_abs;
2021-10-04, by wenzelm
tuned;
2021-10-04, by wenzelm
tuned proofs;
2021-10-04, by wenzelm
more standard binder syntax;
2021-10-04, by wenzelm
clarified 'let' syntax: avoid conflict with existing 'let' in FOL;
2021-10-04, by wenzelm
tuned;
2021-10-04, by wenzelm
tuned;
2021-10-04, by wenzelm
merged
2021-10-04, by paulson
removal of a redundant theorem (and white space)
2021-10-04, by paulson
new material from the Roth development, mostly about finite sets, disjoint famillies and partitions
2021-10-04, by paulson
clarified and updated for release;
2021-10-04, by wenzelm
formal comment concerning 83d2208252d1 vs. d8dc8fdc46fc;
2021-10-04, by wenzelm
more NEWS and CONTRIBUTORS;
2021-10-04, by wenzelm
clarified comments;
2021-10-04, by wenzelm
support symbol \<Parallel>, based on \bigparallel from stdmaryd (stmary10.pfb: move y=1100, scale 222%, embolden by 40 units, adjust spacing);
2021-10-04, by wenzelm
clarified dependencies;
2021-10-04, by wenzelm
updated for release;
2021-10-03, by wenzelm
Added tag Isabelle2021-1-RC0 for changeset fedc0b659881
2021-10-03, by isatest
provide Isabelle/jEdit plugins as services, and thus allow user components do the same;
2021-10-02, by wenzelm
merged
2021-10-02, by wenzelm
updated for release;
2021-10-02, by wenzelm
misc tuning for release;
2021-10-02, by wenzelm
update dependency;
2021-10-02, by wenzelm
trim whitespace;
2021-10-02, by wenzelm
misc tuning for release;
2021-10-02, by wenzelm
misc tuning for release;
2021-10-02, by wenzelm
isabelle build_components -u;
2021-10-02, by wenzelm
updated to Haskell Stach lts-18.12 with GHC ghc-8.10.7;
2021-10-02, by wenzelm
updated to current Cygwin, near 3.2.0;
2021-10-02, by wenzelm
updated to sumatra_pdf-3.3.3;
2021-10-02, by wenzelm
updated default version;
2021-10-02, by wenzelm
updated to xz-java-1.9;
2021-10-02, by wenzelm
updated to sqlite-jdbc-3.36.0.3;
2021-10-02, by wenzelm
updated to postgresql-42.2.24;
2021-10-02, by wenzelm
updated to jfreechart-1.5.3;
2021-10-02, by wenzelm
updated to flatlaf-1.6;
2021-10-02, by wenzelm
clarified signature;
2021-10-02, by wenzelm
clarified Term.dest_abs (again, refining 71dfb835025d): only Free names are relevant for abstract terms, without syntax;
2021-10-02, by wenzelm
clarified sledgehammer_provers, following d8dc8fdc46fc;
2021-10-02, by wenzelm
proper term operation Term.dest_abs;
2021-10-02, by wenzelm
tuned, following Syntax_Trans.variant_abs;
2021-10-02, by wenzelm
proper patterns for (- numeral t), amending 03ff4d1e6784;
2021-10-02, by wenzelm
tuned;
2021-10-02, by wenzelm
merged
2021-10-01, by Mathias Fleury
update syntax for verit
2021-10-01, by Mathias Fleury
clarified antiquotations;
2021-10-01, by wenzelm
clarified antiquotations;
2021-10-01, by wenzelm
provide verit-2021.06-rmx;
2021-10-01, by wenzelm
clarified antiquotations;
2021-09-29, by wenzelm
merged
2021-09-29, by wenzelm
clarified antiquotations;
2021-09-29, by wenzelm
clarified antiquotations;
2021-09-29, by wenzelm
clarified antiquotations;
2021-09-29, by wenzelm
merged
2021-09-29, by desharna
tuned TPTP parsing of THF function application
2021-09-28, by desharna
clarified examples;
2021-09-29, by wenzelm
repaired slip
2021-09-29, by haftmann
merged
2021-09-29, by desharna
updated to Zipperposition 2.1
2021-09-28, by desharna
fixed veriT environment variable in sledgehammer's documentation
2021-09-28, by desharna
avoid overlapping PIDE markup (amending bb25ea271b15);
2021-09-28, by wenzelm
recover some Linux test, using virtual machine node (Ubuntu 20.04, 4 cores, 16 GB);
2021-09-28, by wenzelm
clarified antiquotations;
2021-09-28, by wenzelm
merged
2021-09-28, by wenzelm
clarified antiquotations;
2021-09-28, by wenzelm
clarified antiquotations;
2021-09-28, by wenzelm
clarified antiquotations;
2021-09-28, by wenzelm
clarified antiquotations;
2021-09-28, by wenzelm
clarified antiquotations;
2021-09-28, by wenzelm
clarified positions, notably for ML compiler errors;
2021-09-28, by wenzelm
clarified message;
2021-09-28, by wenzelm
proper default for Sledgehammer GUI panel;
2021-09-28, by wenzelm
tuned antiquotations;
2021-09-28, by wenzelm
more convenient ML arguments: avoid excessive nesting of cartouches;
2021-09-28, by wenzelm
outer syntax: support for control-cartouche tokens;
2021-09-28, by wenzelm
merged
2021-09-28, by nipkow
An example
2021-09-28, by nipkow
prefer veriT over Z3 in sledgehammer
2021-09-28, by desharna
added Zipperposition to sledgehammer's default provers
2021-09-28, by desharna
provide zipperposition-2.1 (still unused);
2021-09-27, by wenzelm
tuned docs
2021-09-27, by blanchet
merged
2021-09-26, by wenzelm
improper proof command 'guess' moved to separate theory "Pure-ex.Guess";
2021-09-26, by wenzelm
NOT is part of syntax bundle also
2021-09-25, by haftmann
merged
2021-09-24, by wenzelm
tuned proofs --- avoid 'guess';
2021-09-24, by wenzelm
apply declarations from interpretations in eigen context also
2021-09-24, by haftmann
grant access to sun.tools.jconsole, as required for Java 17;
2021-09-24, by wenzelm
update to e-2.6, following Martin Desharnais;
2021-09-24, by wenzelm
updated to Metis 2.4 (release 20200713)
2021-09-23, by desharna
avoid problems with launch4j and jdk-17;
2021-09-22, by wenzelm
update to jdk-17+35 (LTS);
2021-09-22, by wenzelm
tuned message;
2021-09-22, by wenzelm
unused since 398b7bb9ebdd;
2021-09-22, by wenzelm
merged
2021-09-22, by desharna
removed checks for non-commercial usage of Vampire as it is now under BSD licence
2021-09-22, by desharna
enabled FOOL for Vampire in Sledgehammer
2021-09-22, by desharna
used Vampire 4.5.1 in Sledgehammer
2021-09-22, by desharna
proper NEWS;
2021-09-22, by wenzelm
tuned NEWS;
2021-09-22, by wenzelm
clarified antiquotations;
2021-09-21, by wenzelm
clarified antiquotations;
2021-09-21, by wenzelm
clarified antiquotations;
2021-09-21, by wenzelm
clarified partial application: immediate check of object-logic, and avoidance of context within closure;
2021-09-21, by wenzelm
merged
2021-09-21, by wenzelm
clarified antiquotations;
2021-09-21, by wenzelm
ML antiquotations for object-logic judgment;
2021-09-21, by wenzelm
proper Sign.const_typargs via Theory.add_deps_const/Theory.const_dep;
2021-09-21, by wenzelm
clarified modules;
2021-09-21, by wenzelm
clarified modules;
2021-09-21, by wenzelm
more uniform syntax;
2021-09-21, by wenzelm
permissive identification, e.g. relevant for HOL-SPARK examples running on rsync-clone;
2021-09-21, by wenzelm
NEWS;
2021-09-21, by wenzelm
bundle lattice_syntax / no_lattice_syntax supersedes theory HOL-Library.Lattice_Syntax;
2021-09-21, by wenzelm
localized command 'syntax' and 'no_syntax';
2021-09-20, by wenzelm
tuned;
2021-09-20, by wenzelm
clarified signature;
2021-09-20, by wenzelm
clarified signature;
2021-09-20, by wenzelm
merged
2021-09-20, by desharna
proper constants in TPTP $let binding
2021-09-20, by desharna
more operations from Isabelle/ML;
2021-09-20, by wenzelm
merged
2021-09-20, by wenzelm
tuned proofs --- eliminated 'guess';
2021-09-20, by wenzelm
tuned proofs;
2021-09-20, by wenzelm
clarified antiquotations;
2021-09-20, by wenzelm
proper firstorderization in Sledgehammer
2021-09-20, by desharna
clarified signature;
2021-09-19, by wenzelm
clarified antiquotations;
2021-09-19, by wenzelm
clarified signature -- prefer antiquotations (with subtle change of exception content);
2021-09-19, by wenzelm
more control symbols;
2021-09-19, by wenzelm
support ML antiquotations with fn abstraction;
2021-09-19, by wenzelm
unused;
2021-09-19, by wenzelm
clarified operations: follow Isabelle/ML more closely;
2021-09-16, by wenzelm
provide current vampire-4.5.1: presently unused in Sledgehammer, but relevant for Isabelle/Naproche;
2021-09-15, by wenzelm
obsolete;
2021-09-15, by wenzelm
tuned;
2021-09-15, by wenzelm
clarified name and options for old vampire-4.2.2;
2021-09-15, by wenzelm
clarified signature;
2021-09-13, by wenzelm
explicit predicate for confined bit range avoids cyclic rewriting in presence of extensionality rule for bit values (contributed by Thomas Sewell)
2021-09-13, by haftmann
more latex macros;
2021-09-13, by wenzelm
tuned;
2021-09-13, by wenzelm
clarified signature;
2021-09-13, by wenzelm
more antiquotations;
2021-09-12, by wenzelm
more antiquotations;
2021-09-12, by wenzelm
more antiquotations;
2021-09-12, by wenzelm
more antiquotations;
2021-09-12, by wenzelm
more antiquotations;
2021-09-12, by wenzelm
clarified antiquotations;
2021-09-12, by wenzelm
more antiquotations;
2021-09-12, by wenzelm
more antiquotations;
2021-09-12, by wenzelm
more antiquotations;
2021-09-11, by wenzelm
clarified antiquotation;
2021-09-11, by wenzelm
more antiquotations;
2021-09-11, by wenzelm
more antiquotations;
2021-09-11, by wenzelm
more antiquotations;
2021-09-11, by wenzelm
tuned;
2021-09-11, by wenzelm
ML antiquotations for type constructors and term constants;
2021-09-11, by wenzelm
more antiquotations;
2021-09-11, by wenzelm
tuned;
2021-09-10, by wenzelm
NEWS;
2021-09-10, by wenzelm
miscellaneous examples and experiments for Isabelle/Pure;
2021-09-10, by wenzelm
tuned comments;
2021-09-10, by wenzelm
unused;
2021-09-10, by wenzelm
clarified order of extra TFrees: underlying fast_string_ord coincides with Name.invent (e.g. from type inference);
2021-09-10, by wenzelm
NEWS;
2021-09-10, by wenzelm
clarified signature: more scalable operations;
2021-09-10, by wenzelm
more scalable operations;
2021-09-09, by wenzelm
more scalable operations;
2021-09-09, by wenzelm
clarified order of extra type variables, following names more often than occurrences;
2021-09-09, by wenzelm
clarified signature;
2021-09-09, by wenzelm
tuned;
2021-09-09, by wenzelm
more scalable operations;
2021-09-09, by wenzelm
omit obsolete field "xs": originally from fd0f8fa2b6bd, but later unused;
2021-09-09, by wenzelm
clarified signature;
2021-09-09, by wenzelm
more robust: client could have terminated already;
2021-09-09, by wenzelm
clarified signature;
2021-09-09, by wenzelm
clarified signature;
2021-09-09, by wenzelm
clarified modules;
2021-09-09, by wenzelm
clarified set of items with order of addition;
2021-09-09, by wenzelm
tuned message;
2021-09-09, by wenzelm
tuned whitespace;
2021-09-09, by wenzelm
clarified signature;
2021-09-09, by wenzelm
tuned;
2021-09-09, by wenzelm
simplified: uniqueness check happens in export_consumer;
2021-09-08, by wenzelm
more markup, e.g. to locate defining theory node in formal document output;
2021-09-07, by wenzelm
tuned signature;
2021-09-07, by wenzelm
export other entities, e.g. relevant for formal document output;
2021-09-07, by wenzelm
pointer_eq_ord: minor performance tuning;
2021-09-07, by wenzelm
more robust: progress.stopped means that build has failed;
2021-09-07, by wenzelm
more reactive interrupt;
2021-09-07, by wenzelm
more reactive interrupt;
2021-09-07, by wenzelm
more robust: retain length of results;
2021-09-07, by wenzelm
more reactive interrupt;
2021-09-07, by wenzelm
tuned signature;
2021-09-07, by wenzelm
tuned signature;
2021-09-07, by wenzelm
tuned signature;
2021-09-07, by wenzelm
tuned;
2021-09-07, by wenzelm
merged
2021-09-07, by wenzelm
clarified modules;
2021-09-06, by wenzelm
more scalable operations;
2021-09-06, by wenzelm
more scalable operations;
2021-09-06, by wenzelm
tuned;
2021-09-06, by wenzelm
clarified modules;
2021-09-06, by wenzelm
clarified signature;
2021-09-06, by wenzelm
more scalable operations;
2021-09-06, by wenzelm
unused;
2021-09-06, by wenzelm
more efficient operations: traverse hyps only when required;
2021-09-06, by wenzelm
more robust signature: result has no particular order;
2021-09-05, by wenzelm
more scalable operations;
2021-09-05, by wenzelm
unused;
2021-09-05, by wenzelm
more scalable operations;
2021-09-05, by wenzelm
clarified;
2021-09-04, by wenzelm
tuned signature;
2021-09-04, by wenzelm
clarified signature;
2021-09-04, by wenzelm
more scalable operations;
2021-09-04, by wenzelm