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
+3000
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.
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
clarified signature;
2021-09-04, by wenzelm
tuned signature;
2021-09-04, by wenzelm
more scalable operations;
2021-09-04, by wenzelm
more scalable operations;
2021-09-04, by wenzelm
more scalable operations;
2021-09-04, by wenzelm
more scalable operations;
2021-09-04, by wenzelm
white space
2021-09-04, by paulson
merged
2021-09-03, by paulson
some fixes connected with card_Diff_singleton
2021-09-03, by paulson
strengthened a few lemmas about finite sets and added a code equation for complex_of_real
2021-09-03, by paulson
tuned;
2021-09-03, by wenzelm
proper inst table;
2021-09-03, by wenzelm
more scalable data structure (but: rarely used many arguments);
2021-09-03, by wenzelm
minor performance tuning: fewer allocations;
2021-09-03, by wenzelm
tuned;
2021-08-31, by wenzelm
more Isabelle/Haskell operations;
2021-08-30, by wenzelm
more Isabelle/Haskell operations;
2021-08-30, by wenzelm
avoid change of existing file, notably rebuild via ghc_stack;
2021-08-30, by wenzelm
tuned signature;
2021-08-30, by wenzelm
more Isabelle/Haskell operations;
2021-08-29, by wenzelm
clarified process description;
2021-08-29, by wenzelm
more Isabelle/Haskell operations;
2021-08-28, by wenzelm
clarified signature;
2021-08-28, by wenzelm
more Isabelle/Haskell;
2021-08-27, by wenzelm
made sure lambda-lifting works well with native let binders in Sledgehammer
2021-08-27, by blanchet
handle Zipperposition's ResourceOut gracefully
2021-08-27, by blanchet
disabled 'ite' in Zipperposition until we upgrade to a version of Zip that supports it and we generate the proper syntax
2021-08-27, by blanchet
proper test for type constructor;
2021-08-26, by wenzelm
more Isabelle/Haskell operations;
2021-08-26, by wenzelm
more Isabelle/Haskell operations;
2021-08-26, by wenzelm
merged
2021-08-26, by wenzelm
tuned;
2021-08-26, by wenzelm
more scalable data structure (but: rarely used with > 5 arguments);
2021-08-26, by wenzelm
Backed out changeset d4af818e0880
2021-08-26, by Kevin Kappelmann
merged
2021-08-25, by wenzelm
more Isabelle/Haskell operations;
2021-08-25, by wenzelm
more Isabelle/Haskell operations;
2021-08-25, by wenzelm
tuned;
2021-08-25, by wenzelm
more Isabelle/Haskell operations;
2021-08-25, by wenzelm
reflect moved theories
2021-08-25, by nipkow
unhide canonical function def examples
2021-08-25, by nipkow
merged
2021-08-25, by nipkow
merged
2021-08-18, by nipkow
Backed out changeset fe8d0f4da0e6
2021-07-09, by nipkow
more Isabelle/Haskell operations;
2021-08-25, by wenzelm
more Isabelle/Haskell operations;
2021-08-24, by wenzelm
more Isabelle/Haskell operations;
2021-08-24, by wenzelm
more Isabelle/Haskell operations;
2021-08-24, by wenzelm
clarified signature;
2021-08-24, by wenzelm
clarified signature;
2021-08-24, by wenzelm
minor performance tuning;
2021-08-24, by wenzelm
tuned;
2021-08-24, by wenzelm
tuned;
2021-08-24, by wenzelm
tuned signature;
2021-08-24, by wenzelm
tuned comments;
2021-08-24, by wenzelm
treat Symbol.eof as in ML (but: presently unused);
2021-08-23, by wenzelm
tuned;
2021-08-23, by wenzelm
minor performance tuning;
2021-08-23, by wenzelm
clarified signature;
2021-08-23, by wenzelm
proper Isabelle symbol positions;
2021-08-23, by wenzelm
more Haskell operations;
2021-08-23, by wenzelm
clarified signature;
2021-08-23, by wenzelm
tuned;
2021-08-23, by wenzelm
tuned;
2021-08-23, by wenzelm
tuned signature: prefer existing Haskell operations;
2021-08-22, by wenzelm
more Haskell operations;
2021-08-22, by wenzelm
tuned signature;
2021-08-22, by wenzelm
tuned comments;
2021-08-22, by wenzelm
tuned;
2021-08-22, by wenzelm
consolidation of rules for bit operations
2021-08-21, by haftmann
fixed $ite syntax in TPTP TFX generation
2021-08-20, by desharna
more Haskell operations;
2021-08-19, by wenzelm
merged
2021-08-19, by wenzelm
revert 0faa68dedce5: very slow;
2021-08-19, by wenzelm
tuned;
2021-08-19, by wenzelm
add/rename some theorems about Map(pings)
2021-08-19, by Lukas Stevens
support configuration options "show_results";
2021-08-18, by wenzelm
consolidate_body more thoroughly, e.g. for reduced ML_Heap.obj_size;
2021-08-18, by wenzelm
merged
2021-08-16, by desharna
fixed $ite syntax in TPTP THX generation
2021-08-16, by desharna
tuned signature;
2021-08-16, by wenzelm
more scalable data structures;
2021-08-16, by wenzelm
more scalable data structures;
2021-08-16, by wenzelm
more scalable data structures;
2021-08-16, by wenzelm
proper position information for Context.theory_data_size;
2021-08-15, by wenzelm
provide bash_process server for Isabelle/ML and other external programs;
2021-08-12, by wenzelm
clarified signature;
2021-08-12, by wenzelm
clarified signature;
2021-08-12, by wenzelm
proper prover_options for batch-build;
2021-08-12, by wenzelm
clarified signature;
2021-08-12, by wenzelm
clarified signature: more options for bash_process;
2021-08-07, by wenzelm
tuned signature;
2021-08-07, by wenzelm
clarified signature;
2021-08-07, by wenzelm
clarified signature;
2021-08-07, by wenzelm
follow phabricator 2021 Week 26;
2021-08-07, by wenzelm
tuned signature;
2021-08-06, by wenzelm
tuned;
2021-08-06, by wenzelm
clarified signature;
2021-08-06, by wenzelm
clarified signature;
2021-08-06, by wenzelm
unused;
2021-08-06, by wenzelm
clarified signature;
2021-08-06, by wenzelm
merged
2021-08-05, by wenzelm
clarified modules;
2021-08-05, by wenzelm
type classes for XML data representation;
2021-08-05, by wenzelm
tuned signature;
2021-08-05, by wenzelm
clarified types: prefer Isabelle byte strings;
2021-08-05, by wenzelm
merged
2021-08-05, by desharna
added option labels to Mirabelle actions
2021-08-05, by desharna
more operations: dest binders;
2021-08-05, by wenzelm
clarified abstract and concrete boolean algebras
2021-08-05, by haftmann
antiquotation for bundles
2021-08-05, by haftmann
prefer persistent hash code for cachable items (see also 72b13af7f266);
2021-08-04, by wenzelm
merged
2021-08-04, by wenzelm
more operations: record overall exported entities;
2021-08-04, by wenzelm
merged
2021-08-04, by desharna
added dummy_fof prover to Sledgehammer
2021-08-04, by desharna
fixed malconfigured option output_dir in mirabelle
2021-08-03, by desharna
merged
2021-08-04, by wenzelm
clarified export of formal entities: name space info is always present, but content depends on option "export_theory";
2021-08-04, by wenzelm
proper name space "kind": this is a formal name, not comment;
2021-08-03, by wenzelm
more uniform signatures in ML and Scala;
2021-08-03, by wenzelm
merged
2021-08-04, by desharna
fixed typo
2021-08-03, by desharna
added dummy_thf prover to Sledgehammer
2021-08-03, by desharna
simplified hierarchy of type classes for bit operations
2021-08-03, by haftmann
obsolete
2021-08-03, by haftmann
more operations, notably free and bound variables as in Isabelle/Pure;
2021-08-03, by wenzelm
more operations on types and terms;
2021-08-02, by wenzelm
clarified jEdit java sources;
2021-08-02, by wenzelm
clarified build.gradle: "compile" stopped working in gradle 6.x / 7.x for unknown reasons;
2021-08-02, by wenzelm
removed junk;
2021-08-02, by wenzelm
moved theory Bit_Operations into Main corpus
2021-08-02, by haftmann
more operations;
2021-08-01, by wenzelm
clarified signature;
2021-08-01, by wenzelm
clarified signature;
2021-08-01, by wenzelm
organize syntax for word operations in bundles
2021-08-01, by haftmann
support for Lazy.Text;
2021-07-31, by wenzelm
prefer compact Isabelle.Bytes;
2021-07-31, by wenzelm
clarified signature;
2021-07-31, by wenzelm
clarified signature --- more operations;
2021-07-31, by wenzelm
tuned;
2021-07-31, by wenzelm
clarified order of modules;
2021-07-31, by wenzelm
more operations;
2021-07-31, by wenzelm
tuned;
2021-07-31, by wenzelm
clarified signature;
2021-07-30, by wenzelm
tuned signature;
2021-07-30, by wenzelm
clarified signature;
2021-07-30, by wenzelm
merged
2021-07-30, by wenzelm
prefer Isabelle.Bytes, based on ShortByteString;
2021-07-28, by wenzelm
tuned;
2021-07-28, by wenzelm
tuned signature;
2021-07-28, by wenzelm
tuned signature: more generic operations;
2021-07-28, by wenzelm
prefer UTF8 implementation from Data.Text.Encoding (foreign C);
2021-07-28, by wenzelm
documented Mirabelle_Sledgehammer's new keep semantics
2021-07-29, by desharna
changed Mirabelle_Sledgehammer keep option from path to boolean
2021-07-28, by desharna
added automatic uniform stride option to Mirabelle
2021-07-28, by desharna
fixed HOL-ex following a5bab59d580b
2021-07-28, by desharna
added support for TFX $let to Sledgehammer's TPTP output
2021-07-27, by desharna
merged
2021-07-27, by desharna
fixed TFX generation when universal quantifier is used as term
2021-07-27, by desharna
merged
2021-07-27, by wenzelm
various improvements of "isabelle scala_project";
2021-07-27, by wenzelm
support for native symlinks on Windows;
2021-07-27, by wenzelm
tuned Mirabelle's theory selection
2021-07-27, by desharna
clarified signature;
2021-07-26, by wenzelm
clarified signature;
2021-07-26, by wenzelm
updated for Isabelle2021 release;
2021-07-25, by wenzelm
back to stackage lts-17.10, to make this work on vmnipkow9 (Windows Server 2012 R2);
2021-07-25, by wenzelm
update to Haskell stack-2.7.3 and stackage lts-17.15;
2021-07-25, by wenzelm
clarified version: Apple now counts like 11, 12, ...;
2021-07-25, by wenzelm
clarified signature;
2021-07-24, by wenzelm
clarified compiler output: allow multithreaded execution;
2021-07-24, by wenzelm
clarified signature: more operations;
2021-07-24, by wenzelm
clarified props: more permissive;
2021-07-24, by wenzelm
more robust;
2021-07-24, by wenzelm
clarified properties: "module" and "no_build";
2021-07-24, by wenzelm
clarified signature;
2021-07-24, by wenzelm
clarified signature;
2021-07-24, by wenzelm
tuned comments;
2021-07-24, by wenzelm
tuned document;
2021-07-24, by wenzelm
clarified names (again), e.g. relevant for "Plugin Options";
2021-07-23, by wenzelm
added simp_options to meson
2021-07-22, by desharna
tuning
2021-07-19, by blanchet
parse TPTP operator @ also when not parenthesized
2021-07-19, by blanchet
removed setup for outdated CVC3 from Isabelle
2021-07-19, by blanchet
tuned E's lambda encoding
2021-07-19, by blanchet
use Vampire's clausifier with iProver, now that E's is no longer supported
2021-07-19, by blanchet
updated Sledgehammer docs -- removed most version numbers since these are tedious to maintain
2021-07-19, by blanchet
compile
2021-07-19, by blanchet
tuned;
2021-07-18, by wenzelm
NEWS;
2021-07-18, by wenzelm
updated documentation on Isabelle/Scala;
2021-07-18, by wenzelm
discontinued obsolete Apple (deprecated);
2021-07-18, by wenzelm
clarified component setup: exclude jar from active component, but use sources from template within ISABELLE_HOME (relevant for "isabelle scala_project -L");
2021-07-18, by wenzelm
more robust "isabelle build_scala" as separate tool;
2021-07-18, by wenzelm
tuned --- based on hints by IntelliJ IDEA;
2021-07-17, by wenzelm
more robust: avoid -D ~~/AFP/thys after crash of AFP.init (notably in AFP/1001c0dfced0);
2021-07-17, by wenzelm
more portable across history;
2021-07-17, by wenzelm
proper isabelle.setup.Setup build;
2021-07-17, by wenzelm
rebuild component;
2021-07-17, by wenzelm
more complete scala_project, including Isabelle/jEdit plugins;
2021-07-17, by wenzelm
clarified directories;
2021-07-17, by wenzelm
more accurate scala_project, based on build.props of components;
2021-07-17, by wenzelm
clarified build_props: empty module means no build;
2021-07-17, by wenzelm
tuned;
2021-07-17, by wenzelm
CONTRIBUTORS
2021-07-17, by haftmann
merged
2021-07-16, by wenzelm
more robust;
2021-07-16, by wenzelm
rebuild component;
2021-07-16, by wenzelm
more robust: for the sake of Isabelle.app on macOS;
2021-07-16, by wenzelm
more robust;
2021-07-16, by wenzelm
more robust;
2021-07-16, by wenzelm
more robust;
2021-07-16, by wenzelm
rebuild component;
2021-07-16, by wenzelm
more informative errors: capture low-level compiler output;
2021-07-16, by wenzelm
more direct isabelle_scala_build: always enabled, no "Admin" requirement;
2021-07-16, by wenzelm
tuned --- fewer warnings;
2021-07-16, by wenzelm
clarified names;
2021-07-16, by wenzelm
tuned --- fewer warnings;
2021-07-16, by wenzelm
clarified directory;
2021-07-16, by wenzelm
clarified names;
2021-07-16, by wenzelm
clarified component setup for old graph browser;
2021-07-16, by wenzelm
redundant: *.class and *.jar are already ignored;
2021-07-16, by wenzelm
proper cat_lines: avoid last "\n";
2021-07-16, by wenzelm
merged
2021-07-16, by paulson
A few new lemmas and simplifications
2021-07-16, by paulson
removed support for experimental Pirate prover
2021-07-16, by blanchet
get rid of remote_vampire since it's hard, if possible at all, to follow Vampire's online options
2021-07-16, by blanchet
merged
2021-07-15, by wenzelm
NEWS;
2021-07-15, by wenzelm
proper example;
2021-07-15, by wenzelm
more tests;
2021-07-15, by wenzelm
more robust: component might be absent;
2021-07-15, by wenzelm
clarified global state: allow to deactivate main plugin;
2021-07-15, by wenzelm
more robust (again): allow to deactivate main plugin;
2021-07-15, by wenzelm
tuned signature;
2021-07-15, by wenzelm
more complete dockables;
2021-07-15, by wenzelm
more robust (see 4d91b6d5d49c);
2021-07-15, by wenzelm
clarified startup: implicitly enforce activation of isabelle.jedit_main.Plugin;
2021-07-15, by wenzelm
more robust;
2021-07-15, by wenzelm
tuned;
2021-07-15, by wenzelm
avoid non-standard encoding;
2021-07-15, by wenzelm
proper cross-platform build: jdk component is required for ISABELLE_SETUP_CLASSPATH in other_isabelle;
2021-07-15, by wenzelm
more robust classpath: skip empty entries;
2021-07-15, by wenzelm
more robust: avoid duplicate classpath entries;
2021-07-15, by wenzelm
build.props for isabelle.jar, including isabelle.jedit;
2021-07-15, by wenzelm
more robust;
2021-07-15, by wenzelm
more portable: avoid Windows CRLF in classpath output;
2021-07-15, by wenzelm
proper lines (amending 59b6f0462086);
2021-07-15, by wenzelm
more systematic treatment of encodings;
2021-07-14, by wenzelm
tuned;
2021-07-14, by wenzelm
extended the 'corec' format slightly
2021-07-15, by blanchet
prefer 'xxx' to 'xxx.yyy' to 'xxx(2)' in Sledgehammer, to some extent
2021-07-14, by blanchet
tuning
2021-07-14, by blanchet
rephrase Nitpick constraint in more first-order format that's also more friendly to the 'box' option
2021-07-14, by blanchet
correctly translate constructor argument in 'primrec'
2021-07-14, by blanchet
simplified a few proofs
2021-07-13, by paulson
revisited ac28714b7478: more faithful preplaying with chained facts
2021-07-13, by blanchet
less
more
|
(0)
-30000
-10000
-3000
-1000
-480
+480
+1000
+3000
tip