Mercurial
Mercurial
>
repos
>
isabelle
/ graph
summary
|
shortlog
|
changelog
| graph |
tags
|
bookmarks
|
branches
|
files
|
gz
|
help
less
more
|
(0)
-30000
-10000
-3000
-1000
-960
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.
revived 'try0' and 'smart' Isar proofs in Sledgehammer
default
tip
10 hours ago, by blanchet
Cleanup of NonstandardAnalysis
16 hours ago, by paulson
A bit of cleaning up
28 hours ago, by paulson
The same, without adding a new simprule
37 hours ago, by paulson
moved some material from Sum_of_Powers
2 days ago, by paulson
merged
2 days ago, by wenzelm
clarified signature;
2 days ago, by wenzelm
clarified theory_names with exported content;
2 days ago, by wenzelm
proper export theory_names: theory/parents are not necessarily present (amending 4d27b520622a);
2 days ago, by wenzelm
proper treatment of empty lines (amending 08f89f0e8a62);
2 days ago, by wenzelm
clarified signature: avoid confusing operation name (amending 8cf14d4ebec4);
2 days ago, by wenzelm
merged
2 days ago, by paulson
The right way to formulate card_UNION, plus the old version for compatibility
3 days ago, by paulson
tuned comments;
3 days ago, by wenzelm
tuned signature;
3 days ago, by wenzelm
clarified signature;
3 days ago, by wenzelm
clarified signature;
3 days ago, by wenzelm
clarified signature;
3 days ago, by wenzelm
unused;
3 days ago, by wenzelm
clarified modules;
3 days ago, by wenzelm
clarified signature;
3 days ago, by wenzelm
clarified signature: more explicit types;
3 days ago, by wenzelm
clarified signature --- avoid dependent types;
3 days ago, by wenzelm
tuned whitespace;
3 days ago, by wenzelm
clarified signature: avoid public representation;
3 days ago, by wenzelm
tuned signature;
3 days ago, by wenzelm
clarified signature;
3 days ago, by wenzelm
unused;
3 days ago, by wenzelm
more accurate treatment of option "editor_output_state", e.g. when changed via Isabelle/jEdit Plugin Options panel;
3 days ago, by wenzelm
clarified signature: more explicit types;
3 days ago, by wenzelm
tuned whitespace;
3 days ago, by wenzelm
tuned, following 298707451ec2;
3 days ago, by wenzelm
unused;
3 days ago, by wenzelm
tuned, following hints by IntelliJ IDEA;
3 days ago, by wenzelm
clarified signature: more explicit types;
3 days ago, by wenzelm
tuned whitespace;
3 days ago, by wenzelm
tuned, following hints by IntelliJ IDEA;
3 days ago, by wenzelm
merged
4 days ago, by wenzelm
more GUI elements;
4 days ago, by wenzelm
clarified signature;
4 days ago, by wenzelm
tuned;
4 days ago, by wenzelm
tuned, following hints by IntelliJ IDEA;
4 days ago, by wenzelm
clarified signature --- more operations;
4 days ago, by wenzelm
clarified signature --- simplified types;
4 days ago, by wenzelm
tuned signature;
4 days ago, by wenzelm
proper toString for Content_XML, which is not covered by trait Content;
4 days ago, by wenzelm
clarified output;
4 days ago, by wenzelm
clarified signature: support different document_session, e.g. within running PIDE session;
4 days ago, by wenzelm
unused (despite cf52379c0776);
4 days ago, by wenzelm
tuned, following hints by IntelliJ IDEA;
4 days ago, by wenzelm
unused (see 696819fe2424);
4 days ago, by wenzelm
clarified signature;
4 days ago, by wenzelm
basic setup for document build panel;
4 days ago, by wenzelm
tuned, following hints by IntelliJ IDEA;
4 days ago, by wenzelm
tuned, following hints by IntelliJ IDEA;
4 days ago, by wenzelm
tuned;
4 days ago, by wenzelm
clarified signature;
4 days ago, by wenzelm
tuned, following hints by IntelliJ IDEA;
4 days ago, by wenzelm
tuned, following hints by IntelliJ IDEA;
4 days ago, by wenzelm
tuned signature;
4 days ago, by wenzelm
tuned signature;
4 days ago, by wenzelm
tuned signature, following hints by IntelliJ IDEA;
4 days ago, by wenzelm
added support for cvc5 (whose interface is almost identical to CVC4)
4 days ago, by blanchet
removing the [simp] attribute breaks too many AFP entries severely
5 days ago, by nipkow
nlists is picked up automatically but conflicts with the RBT setup
5 days ago, by nipkow
new lemma
5 days ago, by nipkow
merged
5 days ago, by nipkow
New theory of fixed length lists
6 days ago, by nipkow
Further streamlining of quick-and-dirty evaluation.
6 days ago, by haftmann
more correct approximation (contributed by Achim Brucker)
3 weeks ago, by Achim D. Brucker
Added tag Isabelle2022-RC0 for changeset b42e20adaeed
8 days ago, by wenzelm
proper Java/Scala compiler classpath for standalone application (see also make_isabelle_app() in Pure/Admin/build_release.scala);
Isabelle2022-RC0
8 days ago, by wenzelm
clarified message;
8 days ago, by wenzelm
provide naproche-20220808 (inactive);
8 days ago, by wenzelm
more robust data representation: notably for Store.read_session_timing with database_server;
8 days ago, by wenzelm
tuned message;
9 days ago, by wenzelm
afford default cache policy, despite 6a29709906c6;
9 days ago, by wenzelm
tuned signature;
9 days ago, by wenzelm
clarified signature: more uniform treatment of cache for Export.read_session vs. Export.read_theory;
9 days ago, by wenzelm
tuned;
9 days ago, by wenzelm
tuned signature;
9 days ago, by wenzelm
clarified signature;
9 days ago, by wenzelm
clarified modules;
9 days ago, by wenzelm
merged
10 days ago, by wenzelm
tuned;
10 days ago, by wenzelm
clarified message;
10 days ago, by wenzelm
clarified signature: prefer Export.Session_Context over Sessions.Database_Context;
10 days ago, by wenzelm
clarified signature: prefer Export.Context;
10 days ago, by wenzelm
clarified signature: find session_database within Session_Context.db_hierarchy;
10 days ago, by wenzelm
clarified signature: prefer Export.Session_Context;
10 days ago, by wenzelm
prefer Export.Context/Session_Context/Theory_Context over Sessions.Database_Context;
10 days ago, by wenzelm
clarified signature;
10 days ago, by wenzelm
tuned signature, following hints by IntelliJ IDEA;
10 days ago, by wenzelm
clarified signature: more robust treatment of server;
10 days ago, by wenzelm
discontinued Export.Provider in favour of Export.Context and its derivatives;
11 days ago, by wenzelm
clarified signature: less redundant -- Sessions.Base_Info already specifies the main session;
11 days ago, by wenzelm
tuned signature: more operations;
11 days ago, by wenzelm
misc tuning and clarification;
11 days ago, by wenzelm
clarified Document.Snapshot.all_exports: refer to material from this (virtual) session;
11 days ago, by wenzelm
clarified database query: refer to semantic theories;
11 days ago, by wenzelm
clarified signature: more operations;
11 days ago, by wenzelm
clarified signature: persistent theory_names in lexical order;
11 days ago, by wenzelm
proper session_databases for database_server: need to follow precise session_hierarchy;
11 days ago, by wenzelm
redundant;
11 days ago, by wenzelm
clarified signature: more robust close operation;
11 days ago, by wenzelm
more uniform exports: proper encoding of empty parents for Pure;
11 days ago, by wenzelm
clarified signature: more uniform treatment of empty exports;
11 days ago, by wenzelm
clarified session name: treat PIDE session as Sessions.DRAFT with imports from other sessions;
11 days ago, by wenzelm
more robust build_hierarchy: support Resources.empty / Sessions.Structure.empty (required for Build_Job.print_log);
11 days ago, by wenzelm
clarified context for retrieval: more explicit types, with optional close() operation;
12 days ago, by wenzelm
tuned;
12 days ago, by wenzelm
unused;
12 days ago, by wenzelm
retrieve information about used files;
12 days ago, by wenzelm
tuned signature -- more robust;
12 days ago, by wenzelm
tuned signature;
12 days ago, by wenzelm
clarified signature: Export.Provider knows its (accidental) theory_names;
12 days ago, by wenzelm
clarified signature;
12 days ago, by wenzelm
tuned, following hints by IntelliJ IDEA;
12 days ago, by wenzelm
clarified signature: proper session_name for Sessions.Base (like Sessions.Info);
12 days ago, by wenzelm
tuned signature;
12 days ago, by wenzelm
clarified signature;
13 days ago, by wenzelm
clarified signature;
13 days ago, by wenzelm
clarified signature;
13 days ago, by wenzelm
avoid multiple load_commands;
13 days ago, by wenzelm
avoid redundant dependencies.load_commands with potential errors (amending ea4f86914cb2);
13 days ago, by wenzelm
tuned signature -- avoid redundant arguments;
13 days ago, by wenzelm
tuned -- following hints by IntelliJ IDEA;
13 days ago, by wenzelm
tuned signature;
13 days ago, by wenzelm
tuned comments;
13 days ago, by wenzelm
removed somewhat pointless transaction: db is meant to be finished (or updated monotonically);
13 days ago, by wenzelm
tuned signature;
2 weeks ago, by wenzelm
clarified signature;
2 weeks ago, by wenzelm
clarified signature: avoid repeated db_context.input_database;
2 weeks ago, by wenzelm
clarified signature: more robust;
2 weeks ago, by wenzelm
removed somewhat pointless operations (see a6c69599ab99);
2 weeks ago, by wenzelm
clarified signature;
2 weeks ago, by wenzelm
tuned;
2 weeks ago, by wenzelm
tuned;
2 weeks ago, by wenzelm
clarified signature;
2 weeks ago, by wenzelm
clarified names;
2 weeks ago, by wenzelm
clarified signature;
2 weeks ago, by wenzelm
clarified names;
2 weeks ago, by wenzelm
clarified signature;
2 weeks ago, by wenzelm
clarified signature: more explicit types;
2 weeks ago, by wenzelm
unused (see 0d30ea76756c);
2 weeks ago, by wenzelm
tuned;
2 weeks ago, by wenzelm
clarified signature;
2 weeks ago, by wenzelm
tuned;
2 weeks ago, by wenzelm
unused (see 3064e165c660);
2 weeks ago, by wenzelm
merge
2 weeks ago, by blanchet
changed the order of Zipperposition slices in Sledgehammer
2 weeks ago, by blanchet
merged
2 weeks ago, by paulson
The wellordering instantiation for length-ordered lists
2 weeks ago, by paulson
show sum_list defn
2 weeks ago, by nipkow
prettified def
2 weeks ago, by nipkow
More lemmas.
2 weeks ago, by haftmann
Some more proofs.
2 weeks ago, by haftmann
a few new theorems
2 weeks ago, by paulson
tuned;
2 weeks ago, by wenzelm
clarified while-loops;
2 weeks ago, by wenzelm
updated to postgresql-42.4.0;
2 weeks ago, by wenzelm
updated to flatlaf-2.4;
2 weeks ago, by wenzelm
updated to pdfjs-2.14.305;
2 weeks ago, by wenzelm
more robust: retain Classpath value;
2 weeks ago, by wenzelm
tuned;
2 weeks ago, by wenzelm
mor robust;
2 weeks ago, by wenzelm
clarified modules;
2 weeks ago, by wenzelm
clarified signature;
2 weeks ago, by wenzelm
update documentation, following 21c1f82e7f5d;
3 weeks ago, by wenzelm
proper classpath for Scala compiler invocation (amending 14e22b525b13);
3 weeks ago, by wenzelm
merged
3 weeks ago, by wenzelm
support for dynamic classpath from exports;
3 weeks ago, by wenzelm
clarified signature;
3 weeks ago, by wenzelm
tuned signature;
3 weeks ago, by wenzelm
Avoid shadowing original List._ namespace.
3 weeks ago, by haftmann
replaced complicated lemma by a simpler one
3 weeks ago, by nipkow
clarified signature;
3 weeks ago, by wenzelm
clarified modules;
3 weeks ago, by wenzelm
merged
3 weeks ago, by wenzelm
more documentation;
3 weeks ago, by wenzelm
tuned;
3 weeks ago, by wenzelm
removed obsolete commands;
3 weeks ago, by wenzelm
command 'scala_build_generated_files' with proper management of source dependencies;
3 weeks ago, by wenzelm
clarified signature;
3 weeks ago, by wenzelm
tuned messages;
3 weeks ago, by wenzelm
support more file types;
3 weeks ago, by wenzelm
support for Java language;
3 weeks ago, by wenzelm
clarified signature;
5 weeks ago, by wenzelm
clarified signature;
5 weeks ago, by wenzelm
support for classpath artifacts within session structure:
5 weeks ago, by wenzelm
clarified names;
5 weeks ago, by wenzelm
clarified signature;
5 weeks ago, by wenzelm
clarified signature;
5 weeks ago, by wenzelm
clarified signature;
5 weeks ago, by wenzelm
clarified signature;
5 weeks ago, by wenzelm
unused;
5 weeks ago, by wenzelm
clarified signature;
5 weeks ago, by wenzelm
tuned signature: more explicit types;
5 weeks ago, by wenzelm
fix document build error
3 weeks ago, by Lukas Stevens
tuned (some HOL lints, by Yecine Megdiche);
3 weeks ago, by Fabian Huch
moved lemma fromm AFP
4 weeks ago, by nipkow
tuned names
4 weeks ago, by nipkow
refined code equations for characters
5 weeks ago, by haftmann
prefer non-JNI SAT solvers by default in Nitpick
5 weeks ago, by blanchet
milder Sledgehammer messages
5 weeks ago, by blanchet
moved lemmas from AFP
5 weeks ago, by nipkow
refined code equations for characters
5 weeks ago, by haftmann
tuned comments;
5 weeks ago, by wenzelm
support for Isabelle/Scala/Java modules in Isabelle/ML;
5 weeks ago, by wenzelm
more robust Scala 3 indentation, for the sake of IntelliJ IDEA;
5 weeks ago, by wenzelm
clarified signature: read_theory_exports is already ordered;
5 weeks ago, by wenzelm
clarified signature;
5 weeks ago, by wenzelm
tuned;
5 weeks ago, by wenzelm
sketch for word-specific lsb and msb
5 weeks ago, by haftmann
switch to Scala 3;
6 weeks ago, by wenzelm
minor performance tuning: avoid redundant BigInt construction;
5 weeks ago, by wenzelm
added lemmas total_on_trancl and totalp_on_tranclp
6 weeks ago, by desharna
Move code lemmas for symbolic computation of bit operations on int to distribution.
6 weeks ago, by haftmann
fixed diverging simproc cont_intro
6 weeks ago, by desharna
corrections and adjustions for Scala 3
6 weeks ago, by haftmann
more complete set of code equations
6 weeks ago, by haftmann
officical abstract characters for code generation
6 weeks ago, by haftmann
provide components for scala3 (still inactive);
6 weeks ago, by wenzelm
updated download version;
6 weeks ago, by wenzelm
obsolete;
6 weeks ago, by wenzelm
more keywords for scala3;
6 weeks ago, by wenzelm
discontinued Isabelle tools implemented as .scala scripts;
6 weeks ago, by wenzelm
tuned proofs
6 weeks ago, by desharna
clarified heap alignment, to make it potentially more stable on macOS;
6 weeks ago, by wenzelm
tuned proof
6 weeks ago, by desharna
added lemmas domain_comp and unify_gives_minimal_domain
6 weeks ago, by desharna
added definition range_vars and lemmas vars_of_subst_conv_Union, vars_of_subst_subset, range_vars_comp_subset, and unify_gives_minimal_range
6 weeks ago, by desharna
merged
6 weeks ago, by desharna
added definition IMGU and lemmas IMGU_iff_Idem_and_MGU and unify_computes_IMGU
6 weeks ago, by desharna
more macOS versions;
6 weeks ago, by wenzelm
prefer Isabelle/Scala operations;
7 weeks ago, by wenzelm
merged
7 weeks ago, by wenzelm
clarified IO, following Java 11 and Isabelle/Scala;
7 weeks ago, by wenzelm
prefer Scala operations;
7 weeks ago, by wenzelm
minor tuning;
7 weeks ago, by wenzelm
switched to statically compiled ci profile;
8 weeks ago, by Fabian Huch
more operations on Bytes.T;
7 weeks ago, by wenzelm
more operations on Bytes.T;
7 weeks ago, by wenzelm
tuned BNF bounds for function space and bounded sets; NEWS and CONTRIBUTORS
7 weeks ago, by traytel
strict bounds for BNFs (by Jan van Brügge)
7 weeks ago, by traytel
More lemmas.
7 weeks ago, by haftmann
Centralized some char-related lemmas in distribution.
7 weeks ago, by haftmann
prefer antiquotations;
7 weeks ago, by wenzelm
clarified modules;
7 weeks ago, by wenzelm
more documentation;
7 weeks ago, by wenzelm
merged
7 weeks ago, by wenzelm
tuned whitespace;
7 weeks ago, by wenzelm
clarified signature: File.read_lines is based on scalable Bytes.T;
7 weeks ago, by wenzelm
clarified modules;
7 weeks ago, by wenzelm
prefer scalable Bytes.T;
7 weeks ago, by wenzelm
unused;
7 weeks ago, by wenzelm
prefer scalable Bytes.T;
7 weeks ago, by wenzelm
missing recursive let-expansion in SMT translation
7 weeks ago, by Mathias Fleury
merged
7 weeks ago, by desharna
added lemma monotone_on_o
7 weeks ago, by desharna
redefined mono_on and strict_mono_on as an abbreviation of monotone_on
7 weeks ago, by desharna
changed argument order of mono_on and strict_mono_on to uniformize with monotone_on and other predicates
7 weeks ago, by desharna
more robust CSV syntax, e.g. for "pull_date";
7 weeks ago, by wenzelm
merged
7 weeks ago, by wenzelm
more scalable generated files and code export, using Bytes.T;
7 weeks ago, by wenzelm
more operations;
7 weeks ago, by wenzelm
proper execution of Bytes.write;
7 weeks ago, by wenzelm
Avoid calculations where not necessary.
7 weeks ago, by haftmann
Prefer existing horner sum combinator.
7 weeks ago, by haftmann
Executable lexords.
7 weeks ago, by haftmann
Less warnings.
7 weeks ago, by haftmann
merged
7 weeks ago, by wenzelm
more operations;
7 weeks ago, by wenzelm
removed unused operations;
7 weeks ago, by wenzelm
clarified signature: more operations;
7 weeks ago, by wenzelm
tuned;
7 weeks ago, by wenzelm
tuned comments;
7 weeks ago, by wenzelm
tuned;
7 weeks ago, by wenzelm
clarified session resources for bootstrap, notably for Scala functions;
7 weeks ago, by wenzelm
tuned;
7 weeks ago, by wenzelm
clarified signature;
7 weeks ago, by wenzelm
tuned signature;
7 weeks ago, by wenzelm
clarified types and defaults;
7 weeks ago, by wenzelm
merged
7 weeks ago, by desharna
added lemmas monotone{,_on}_multp_multp_image_mset
8 weeks ago, by desharna
added lemmas monotone_on_empty[simp] and monotone_on_subset
8 weeks ago, by desharna
added predicate monotone_on and redefined monotone to be an abbreviation.
8 weeks ago, by desharna
merged
8 weeks ago, by wenzelm
NEWS;
8 weeks ago, by wenzelm
support XZ compression in Isabelle/ML;
8 weeks ago, by wenzelm
prefer scalable byte strings;
8 weeks ago, by wenzelm
more scalable byte messages, notably for Scala functions in ML;
8 weeks ago, by wenzelm
tuned comments;
8 weeks ago, by wenzelm
clarified ML pretty printing;
8 weeks ago, by wenzelm
clarified signature: more operations;
8 weeks ago, by wenzelm
tuned signature;
8 weeks ago, by wenzelm
tuned comments;
8 weeks ago, by wenzelm
tuned signature: more operations;
8 weeks ago, by wenzelm
tuned signature: more operations;
8 weeks ago, by wenzelm
tuned signature;
8 weeks ago, by wenzelm
clarified signature: avoid repeated string copying via Substring.slice;
8 weeks ago, by wenzelm
support for scalable byte strings, with incremental construction;
8 weeks ago, by wenzelm
clarified signature;
8 weeks ago, by wenzelm
remove unused file following 51e696887b81;
8 weeks ago, by wenzelm
added lemma map_mono_strict_suffix
8 weeks ago, by desharna
more robust: always override ISABELLE_IDENTIFIER from environment;
2 months ago, by wenzelm
"isabelle vscode" is regular user-space tool;
2 months ago, by wenzelm
fix veriT reconstruction for and_pos and lambda-lifting
2 months ago, by Mathias Fleury
added lemmas image_mset_eq_{image_mset_plus,plus,plus_image_mset}D, and multp_image_mset_image_msetD
2 months ago, by desharna
clarified options of "isabelle hg_sync" vs. "isabelle sync";
2 months ago, by wenzelm
tuned layout;
2 months ago, by wenzelm
misc tuning;
2 months ago, by wenzelm
clarified document structure;
2 months ago, by wenzelm
promote "isabelle sync" to regular user-space tool, with proper documentation;
2 months ago, by wenzelm
more comments;
2 months ago, by wenzelm
more options;
2 months ago, by wenzelm
sync session images, based on accidental local state;
2 months ago, by wenzelm
more informative release_snapshot, to see better where the cronjob fails;
2 months ago, by wenzelm
more robust, notably for crontab;
2 months ago, by wenzelm
clarified names;
2 months ago, by wenzelm
tuned;
2 months ago, by wenzelm
tuned;
2 months ago, by wenzelm
proper make_port for regular situation;
2 months ago, by wenzelm
clarified types -- proper default_port via make_port;
2 months ago, by wenzelm
proper nominal_port, notably for port forwarding;
2 months ago, by wenzelm
some additional lemmas and a little tidying up
2 months ago, by paulson
merged
2 months ago, by desharna
added lemma totalp_on_total_on_eq[pred_set_conv]
2 months ago, by desharna
added lemma reflp_on_empty[simp] and totalp_on_empty[simp]
2 months ago, by desharna
removed non-standard spaces in output
2 months ago, by nipkow
merged
2 months ago, by wenzelm
avoid noise via context.progress (amending 68162e4f60a7);
2 months ago, by wenzelm
more robust treatment of rsync on macOS (see also 96fb1f9a4042);
2 months ago, by wenzelm
tuned whitespace;
2 months ago, by wenzelm
more robust: no change of directory attributes of initial test, notably target without .hg_sync meta data;
2 months ago, by wenzelm
merged
2 months ago, by desharna
added lemmas reflp_on_Inf and reflp_on_Sup
2 months ago, by desharna
replaced HOL.implies by Pure.imp in reflp_mono for consistency with other lemmas
2 months ago, by desharna
added lemmas reflp_on_inf, reflp_on_sup, and reflp_on_mono
2 months ago, by desharna
merged
2 months ago, by wenzelm
more robust: protect_args does not work with rsync 2.x from macOS, and is not required in typical situations;
2 months ago, by wenzelm
clarified context with global defaults;
2 months ago, by wenzelm
tuned signature;
2 months ago, by wenzelm
clarified signature: more explicit type Rsync.Context;
2 months ago, by wenzelm
clarified signature;
2 months ago, by wenzelm
clarified modules;
2 months ago, by wenzelm
provide python-3.10.4 for darwin and linux;
2 months ago, by Fabian Huch
provide hugo-0.88.1 for darwin and linux;
2 months ago, by Fabian Huch
removed obsolete self_update: always enabled, notably on lxbroy10 which is the only shared-home system (and still requires current isabelle_self);
2 months ago, by wenzelm
avoid redundant meta data: exclude .hg_archival.txt;
2 months ago, by wenzelm
clarified remote vs. local build_history: operate on hg_sync directory instead of repository;
2 months ago, by wenzelm
proper operation on String, not Path;
2 months ago, by wenzelm
clarified signature: cwd can be misleading --- changes meaning of target;
2 months ago, by wenzelm
merged
2 months ago, by wenzelm
more meta data;
2 months ago, by wenzelm
clarified signature: more operations;
2 months ago, by wenzelm
tuned messages;
2 months ago, by wenzelm
provide .hg_sync meta data;
2 months ago, by wenzelm
clarified signature;
2 months ago, by wenzelm
clarified options;
2 months ago, by wenzelm
more robust;
2 months ago, by wenzelm
clarified signature (again);
2 months ago, by wenzelm
clarified signature;
2 months ago, by wenzelm
NEWS
2 months ago, by desharna
added lemmas reflp_on_subset, totalp_on_subset, and total_on_subset
2 months ago, by desharna
introduced predicate reflp_on and redefined reflp to be an abbreviation
2 months ago, by desharna
merged
2 months ago, by nipkow
insort renamings
2 months ago, by nipkow
more operations;
2 months ago, by wenzelm
support explicit SSH port;
2 months ago, by wenzelm
redundant (after f28aee3ad1e6): self_update already takes care of currently active Isabelle clone;
2 months ago, by wenzelm
clarified options;
2 months ago, by wenzelm
Added lemmas
2 months ago, by nipkow
merged
2 months ago, by paulson
Five slightly useful lemmas
2 months ago, by paulson
clarified option -T;
2 months ago, by wenzelm
preserve jars for quick testing;
2 months ago, by wenzelm
tuned names;
2 months ago, by wenzelm
clarified documentation: $ISABELLE_HOME is not a repository for regular releases;
2 months ago, by wenzelm
clarified command-line options;
2 months ago, by wenzelm
proper anchored pattern;
2 months ago, by wenzelm
support thorough check of file content;
2 months ago, by wenzelm
more documentation;
2 months ago, by wenzelm
clarified signature;
2 months ago, by wenzelm
tuned messages;
2 months ago, by wenzelm
tuned whitespace;
2 months ago, by wenzelm
merged
2 months ago, by wenzelm
support to synchronize Isabelle + AFP repositories;
2 months ago, by wenzelm
more robust: local repository required;
2 months ago, by wenzelm
support option -r;
2 months ago, by wenzelm
omit pointless option;
2 months ago, by wenzelm
tuned;
2 months ago, by wenzelm
more documentation;
2 months ago, by wenzelm
support filter rules, notably "protect";
2 months ago, by wenzelm
support for "isabelle hg_sync";
2 months ago, by wenzelm
clarified signature;
2 months ago, by wenzelm
tuned comments;
2 months ago, by wenzelm
clarified signature;
2 months ago, by wenzelm
tuned signature;
2 months ago, by wenzelm
tuned signature;
2 months ago, by wenzelm
support rsync;
2 months ago, by wenzelm
added lemmas Multiset.bex_{least,greatest}_element
2 months ago, by desharna
added predicate totalp_on and abbreviation totalp
2 months ago, by desharna
excluded dummy ATPs from Sledgehammer's default provers
2 months ago, by desharna
move monotone from Complete_Partial_Order to Orderings
2 months ago, by desharna
qualified name to fix integrable_cong ambiguity
2 months ago, by paulson
Renamed the misleading has_field_derivative_iff_has_vector_derivative. Inserted a number of minor lemmas
2 months ago, by paulson
Eliminated two unnecessary inductions
2 months ago, by paulson
NEWS
2 months ago, by desharna
added lemma image_mset_filter_mset_swap
2 months ago, by desharna
merged
2 months ago, by desharna
added lemmas filter_mset_cong{0,}
2 months ago, by desharna
»nil« seems to be a reserved constructor word in PolyML
2 months ago, by haftmann
tidied auto / simp with null arguments
3 months ago, by paulson
tuned signature;
3 months ago, by wenzelm
provide Isabelle/Electron test;
3 months ago, by wenzelm
tuned text;
3 months ago, by wenzelm
tuned text;
3 months ago, by wenzelm
Tidied up some super-messy proofs
3 months ago, by paulson
Added a couple of obvious simprules
3 months ago, by paulson
added lemma
3 months ago, by nipkow
tuned signature: avoid problems with scala3;
3 months ago, by wenzelm
proper indentation;
3 months ago, by wenzelm
merged
3 months ago, by wenzelm
clarified management of interpreter threads: more generic;
3 months ago, by wenzelm
clarified signature;
3 months ago, by wenzelm
clarified signature;
3 months ago, by wenzelm
clarified signature, based on hints by IntelliJ IDEA;
3 months ago, by wenzelm
tuned signature;
3 months ago, by wenzelm
more robust: avoid partiality;
4 months ago, by wenzelm
tuned;
4 months ago, by wenzelm
clarified signature;
4 months ago, by wenzelm
clarified signature;
4 months ago, by wenzelm
tuned --- avoid warnings in scala3;
4 months ago, by wenzelm
clarified signature;
4 months ago, by wenzelm
pass new option only to new version of E
4 months ago, by blanchet
merged
4 months ago, by desharna
reused slice in Sledgehammer's minimizer
4 months ago, by desharna
merged
4 months ago, by wenzelm
revert 2c861b196d52: still required in HOL/Library/Code_Test.thy;
4 months ago, by wenzelm
merged
4 months ago, by wenzelm
tuned --- avoid warnings in scala3;
4 months ago, by wenzelm
tuned --- avoid redundant patterns;
4 months ago, by wenzelm
avoid pattern-match warnings, notably in scala3;
4 months ago, by wenzelm
proper type conversion for scala-2.13: problem was unnoticed since ca17e9ebfdf1;
4 months ago, by wenzelm
tuned --- accomodate scala3;
4 months ago, by wenzelm
proper type conversion for scala-2.13: problem was unnoticed since ca17e9ebfdf1;
4 months ago, by wenzelm
back to more ambitious scala-3.1.1 (see 8b7497992301);
4 months ago, by wenzelm
tuned --- fewer warnings in scala3;
4 months ago, by wenzelm
tuned -- avoid warnings for scala3;
4 months ago, by wenzelm
tuned signature -- avoid warnings for scala3;
4 months ago, by wenzelm
removed unused flag (see 25c6423ec538);
4 months ago, by wenzelm
clarified versions;
4 months ago, by wenzelm
documentation on diagnostic devices for code generation
4 months ago, by haftmann
more correct language
4 months ago, by haftmann
enable an E option suggested by Petar Vukmirovic
4 months ago, by blanchet
used HTTPS for SystemOnTPTP
4 months ago, by desharna
moved from AFP to distribution
4 months ago, by haftmann
avoid static access to sun.tools.jconsole: more robust compilation (notably with scala3), but less robust invocation;
4 months ago, by wenzelm
more operations;
4 months ago, by wenzelm
clarified signature;
4 months ago, by wenzelm
tuned: avoid ambiguity in scala3;
4 months ago, by wenzelm
clarified signature: avoid ambiguity in scala3;
4 months ago, by wenzelm
clarified signature: avoid ambiguity in scala3;
4 months ago, by wenzelm
more robust types (for scala3);
4 months ago, by wenzelm
tuned for scala3;
4 months ago, by wenzelm
proper indentation (relevant for scala3);
4 months ago, by wenzelm
adjusted printing of type annotations to accomodate Scala 3
4 months ago, by haftmann
two new examples
4 months ago, by paulson
pass constructor arity as part of case certficiate
4 months ago, by haftmann
tuned whitespace in generated code
4 months ago, by haftmann
tuned, centralizing case distinction at one place at the cost of modest duplication
4 months ago, by haftmann
clarified formatting, for the sake of scala3;
4 months ago, by wenzelm
merged
4 months ago, by wenzelm
tuned formatting;
4 months ago, by wenzelm
clarified formatting, for the sake of scala3;
4 months ago, by wenzelm
tuned
4 months ago, by haftmann
tuned
4 months ago, by haftmann
merge
4 months ago, by blanchet
tuned slices to get the fifth Zipperposition slice in a typical run
4 months ago, by blanchet
merged
4 months ago, by desharna
tuned sledgehammer documentation
4 months ago, by desharna
tuned spelling;
4 months ago, by wenzelm
merged
4 months ago, by wenzelm
updated to scala-parser-combinators 2.1.0, which also fits to scala-3.0.2;
4 months ago, by wenzelm
clarified invocation of isabelle.setup.Setup: -classpath allows multiple jars, as required for scala3;
4 months ago, by wenzelm
tuned: eliminted do-while for the sake of scala3;
4 months ago, by wenzelm
prefer scala 3.0.x, for option "-source 3.0-migration";
4 months ago, by wenzelm
tuned: avoid problems with scala3;
4 months ago, by wenzelm
tuned: avoid problems with scala3;
4 months ago, by wenzelm
provide SCALA_INTERFACES for isabelle_setup;
4 months ago, by wenzelm
build Isabelle Scala component from official downloads (for scala-3.1.1);
4 months ago, by wenzelm
added documentation
4 months ago, by desharna
merged
4 months ago, by desharna
tuned sledehammer to return best succeeding preplay method
4 months ago, by desharna
expanded sledgehammer's expect option with some_preplayed
4 months ago, by desharna
added preplay results to sledgehammer_output
4 months ago, by desharna
tuned sledgehammer to suggest (smt (verit)) on failing smt preplay for all but Z3
4 months ago, by desharna
further tweaked E's setup
4 months ago, by blanchet
tweaked E setup
4 months ago, by blanchet
merged
4 months ago, by desharna
post-merged into new Lethe code
4 months ago, by desharna
merged
4 months ago, by desharna
fixed generation of Isar proofs e89709b80b6e
4 months ago, by desharna
NEWS and CONTRIBUTORS
4 months ago, by haftmann
nicer TPTP output
4 months ago, by blanchet
regenerated
4 months ago, by haftmann
tighter check to ensure that patterns remain left-linear, previous implementation was overcautious
4 months ago, by haftmann
tuned
4 months ago, by haftmann
tuned
4 months ago, by haftmann
separated treatment of undefined bodys
4 months ago, by haftmann
tuned arguments
4 months ago, by haftmann
modernized handling of variables
4 months ago, by haftmann
structurally tuned
4 months ago, by haftmann
tuned names
4 months ago, by haftmann
prefer build combinator
4 months ago, by haftmann
tuned whitespace
4 months ago, by haftmann
proper option argument;
4 months ago, by wenzelm
prefer Isabelle shasum over the old command-line tool with its extra marker character;
4 months ago, by wenzelm
tuned signature;
4 months ago, by wenzelm
tuned signature;
4 months ago, by wenzelm
tuned text, without update of component for now;
4 months ago, by wenzelm
omit somewhat pointless integrity check;
4 months ago, by wenzelm
tuned;
4 months ago, by wenzelm
compile TPTP module
4 months ago, by blanchet
compile mirabelle
4 months ago, by blanchet
further modernized E setup
4 months ago, by blanchet
cleaned up obsolete E setup and a bit of SPASS
4 months ago, by blanchet
second and last step in making time slicing more flexible in Sledgehammer: try to honor desired slice size
4 months ago, by blanchet
first step in making time slicing more flexible in Sledgehammer: label slices with 'slice size'
4 months ago, by blanchet
updated vscode_extension;
4 months ago, by wenzelm
added parentheses in TPTP output -- seem necessary for some provers
4 months ago, by blanchet
merged
4 months ago, by wenzelm
provide pre-built vscodium-1.65.2 for all platforms;
4 months ago, by wenzelm
tuned;
4 months ago, by wenzelm
provide vscode_extension via component, thus users don't need Node.js development tools;
4 months ago, by wenzelm
clarified options;
4 months ago, by wenzelm
Some new library lemmas
4 months ago, by paulson
merged
4 months ago, by paulson
really removing Dedekind_real
4 months ago, by paulson
merged
4 months ago, by paulson
Moving Dedekind_Real to the AFP
4 months ago, by paulson
tuned
4 months ago, by haftmann
separated case reduction
4 months ago, by haftmann
separated selector function entirely
4 months ago, by haftmann
self-contained extraction auf clauses
4 months ago, by haftmann
extracted selector function, restoring code generation for let expressions
4 months ago, by haftmann
streamlined
4 months ago, by haftmann
streamlined
4 months ago, by haftmann
streamlined
4 months ago, by haftmann
disentangled
4 months ago, by haftmann
merged
4 months ago, by wenzelm
tuned message;
4 months ago, by wenzelm
more operations;
4 months ago, by wenzelm
tuned signature;
4 months ago, by wenzelm
more robust install/uninstall;
4 months ago, by wenzelm
more formal extension_manifest, with shasum for sources;
4 months ago, by wenzelm
tuned;
4 months ago, by wenzelm
tuned signature;
4 months ago, by wenzelm
clarified signature;
4 months ago, by wenzelm
proper usage;
4 months ago, by wenzelm
tuned -- follow sha1_digest in src/Tools/Setup/src/Build.java;
4 months ago, by wenzelm
tuned signature;
4 months ago, by wenzelm
clarified modules;
4 months ago, by wenzelm
tuned signature;
4 months ago, by wenzelm
... and removing Primrec from ROOT too
4 months ago, by paulson
Removal of the Primrec example in preparation for making it an AFP entry
4 months ago, by paulson
merged
4 months ago, by desharna
avoided recomputation in Cooper.djf and ran `isabelle regenerate_cooper`
5 months ago, by desharna
split veriT reconstruction into Lethe and veriTÂ part
5 months ago, by Mathias Fleury
clarified options;
4 months ago, by wenzelm
more robust errors -- on foreground process instead of background server;
4 months ago, by wenzelm
clarified options -l vs. -R;
4 months ago, by wenzelm
command-line arguments for "isabelle vscode", similar to "isabelle jedit";
4 months ago, by wenzelm
proper command-line tool;
4 months ago, by wenzelm
support console output, e.g. "isabelle vscode -C -- --help";
4 months ago, by wenzelm
run Isabelle/VSCode via Scala;
4 months ago, by wenzelm
clarified module name;
4 months ago, by wenzelm
clean build from explicit MANIFEST: avoid accidental garbage in vsix package;
4 months ago, by wenzelm
incorporate build_grammar into build_vscode_extension;
4 months ago, by wenzelm
removed old generated file;
4 months ago, by wenzelm
Tidied several ugly proofs in some elderly examples
5 months ago, by paulson
tuned message;
5 months ago, by wenzelm
clarified errors;
5 months ago, by wenzelm
tuned messages;
5 months ago, by wenzelm
support Node.js as well, reusing the engine from Electron/VSCodium;
5 months ago, by wenzelm
updated to vscode 1.65.2;
5 months ago, by wenzelm
proper result check;
5 months ago, by wenzelm
merged
5 months ago, by wenzelm
clarified directory layout and settings: more robust on all platforms;
5 months ago, by wenzelm
tuned;
5 months ago, by wenzelm
support Electron application framework;
5 months ago, by wenzelm
generated lemma map_ident_strong for BNFs
5 months ago, by desharna
updated SMT certificates
5 months ago, by desharna
used more descriptive assert names in SMT-Lib output
5 months ago, by desharna
clarified and unified executable names;
5 months ago, by wenzelm
tuned;
5 months ago, by wenzelm
tuned;
5 months ago, by wenzelm
merged
5 months ago, by wenzelm
suppress OCaml icons: avoid conflict of .ml and .ML, due to case-insensitive file-names in VSCode;
5 months ago, by wenzelm
fix handling of lambdas in reconstruction of eq_congruent
5 months ago, by Mathias Fleury
more robust: avoid breakdown of Search dialog;
5 months ago, by wenzelm
tuned;
5 months ago, by wenzelm
always use Isabelle encoding, as in Isabelle/jEdit;
5 months ago, by wenzelm
tuned signature;
5 months ago, by wenzelm
clarified signature: more uniform ts vs. Scala;
5 months ago, by wenzelm
discontinued isabelle_filesystem (superseded by isabelle_encoding), see also da1108a6d249;
5 months ago, by wenzelm
actually decode/encode symbols;
5 months ago, by wenzelm
merged
5 months ago, by wenzelm
prefer yarn over npm;
5 months ago, by wenzelm
more accurate .hgignore;
5 months ago, by wenzelm
clarified startup of "isabelle vscode": vscodium component is required, with patches for Isabelle/VSCode;
5 months ago, by wenzelm
tuned messages;
5 months ago, by wenzelm
proper init_resources for macos;
5 months ago, by wenzelm
clarified names;
5 months ago, by wenzelm
clarified modules: vscode vs. extension;
5 months ago, by wenzelm
inline Isabelle symbols into source text, so that "isabelle vscode" can start up properly without access to process.env or fs;
5 months ago, by wenzelm
more operations;
5 months ago, by wenzelm
tuned comments;
5 months ago, by wenzelm
patch VSCode source tree to support isabelle_encoding.ts;
5 months ago, by wenzelm
more robust, pass "yarn valid-layers-check";
5 months ago, by wenzelm
clarified directories;
5 months ago, by wenzelm
patch for vscode encoding "UTF-8-Isabelle": clone of "utf8", no symbols yet;
5 months ago, by wenzelm
fit into vscode source conventions;
5 months ago, by wenzelm
A tiny further cleanup
5 months ago, by paulson
Tidied some messy proofs
5 months ago, by paulson
merged
5 months ago, by nipkow
more count_list lemmas
5 months ago, by nipkow
towards UTF-8-Isabelle symbol encoding;
5 months ago, by wenzelm
updated to VSCode 1.65.0;
5 months ago, by wenzelm
clarified char symbols: cover most European languages;
5 months ago, by wenzelm
more elementary Symbol.Matcher without detour via Regex (see also Pure/General/symbol_explode.ML);
5 months ago, by wenzelm
tuned comments;
5 months ago, by wenzelm
more robust dependencies: avoid implicit update, escpecially of underlying vscode engine;
5 months ago, by wenzelm
proper file headers;
5 months ago, by wenzelm
added count_list lemmas
5 months ago, by nipkow
tuned message;
5 months ago, by wenzelm
more compact result;
5 months ago, by wenzelm
prepare patched version more thoroughly, with explicit patches;
5 months ago, by wenzelm
tuned signature;
5 months ago, by wenzelm
recover platform-specific node binaries from original download, notably for node-pty for Terminal;
5 months ago, by wenzelm
tuned message;
5 months ago, by wenzelm
tuned;
5 months ago, by wenzelm
tuned imports;
5 months ago, by wenzelm
misc tuning and clarification;
5 months ago, by wenzelm
more executable files;
5 months ago, by wenzelm
tuned;
5 months ago, by wenzelm
tuned output;
5 months ago, by wenzelm
clarified signature;
5 months ago, by wenzelm
tuned, based on suggestions by IntelliJ IDEA;
5 months ago, by wenzelm
tuned;
5 months ago, by wenzelm
clarified command-line options;
5 months ago, by wenzelm
update official Isabelle release, notably for "Admin/init -R";
5 months ago, by wenzelm
more robust;
5 months ago, by wenzelm
build component for VSCodium (cross-compiled from sources for all platforms);
5 months ago, by wenzelm
tuned signature: more robust operation;
5 months ago, by wenzelm
clarified order;
5 months ago, by wenzelm
proper antiquotations (amending ff784d5a5bfb);
5 months ago, by wenzelm
clarified signature: file operations take standard_path as in Isabelle/ML/Scala;
5 months ago, by wenzelm
provide symbols statically via ISABELLE_VSCODE_WORKSPACE, instead of LSP/PIDE protocol;
5 months ago, by wenzelm
proper init of non-existing file;
5 months ago, by wenzelm
proper function call;
5 months ago, by wenzelm
clarified signature;
5 months ago, by wenzelm
tuned;
5 months ago, by wenzelm
tuned, based on suggestions by IntelliJ IDEA;
5 months ago, by wenzelm
tuned;
5 months ago, by wenzelm
clarified signature;
5 months ago, by wenzelm
clarified modules: more uniform .scala vs. ts (amending 4519eeefe3b5);
5 months ago, by wenzelm
misc tuning, based on suggestions by IntelliJ IDEA;
5 months ago, by wenzelm
clarified signature;
5 months ago, by wenzelm
tuned signature;
5 months ago, by wenzelm
clarified signature;
5 months ago, by wenzelm
tuned imports;
5 months ago, by wenzelm
clarified signature;
5 months ago, by wenzelm
clarified signature;
5 months ago, by wenzelm
tuned signature;
5 months ago, by wenzelm
misc tuning, based on suggestions by IntelliJ IDEA;
5 months ago, by wenzelm
clarified modules;
5 months ago, by wenzelm
support for file-system operations;
5 months ago, by wenzelm
tuned signature;
5 months ago, by wenzelm
follow standard Isabelle license --- no longer published on market place;
5 months ago, by wenzelm
tuned README;
5 months ago, by wenzelm
disregard public marketplace;
5 months ago, by wenzelm
tuned imports;
5 months ago, by wenzelm
more robust;
5 months ago, by wenzelm
merged
5 months ago, by wenzelm
tuned message;
5 months ago, by wenzelm
clarified module;
5 months ago, by wenzelm
tuned comments;
5 months ago, by wenzelm
added documentation for new VSCode modules;
5 months ago, by Fabian Huch
proper monospace font for terminal;
5 months ago, by wenzelm
merged
5 months ago, by wenzelm
tuned;
5 months ago, by wenzelm
support system path representations (as in Isabelle/Java/Scala);
5 months ago, by wenzelm
auto-update;
5 months ago, by wenzelm
more robust;
5 months ago, by wenzelm
clarified modules;
5 months ago, by wenzelm
clarified rendering;
5 months ago, by wenzelm
prefer hardwired locale;
5 months ago, by wenzelm
more aggressive activation;
5 months ago, by wenzelm
Added some theorems (from Wetzel)
5 months ago, by paulson
tuned;
5 months ago, by wenzelm
tuned;
5 months ago, by wenzelm
tuned message;
5 months ago, by wenzelm
disable extension updates;
5 months ago, by wenzelm
tuned message;
5 months ago, by wenzelm
disable check for updates: support just one static version;
5 months ago, by wenzelm
misc tuning based on comments by Heiko Eißfeldt;
5 months ago, by wenzelm
misc tuning based on comments by Heiko Eißfeldt;
5 months ago, by wenzelm
removed junk;
5 months ago, by wenzelm
some updates to README.md;
5 months ago, by wenzelm
clarified default settings;
5 months ago, by wenzelm
tuned whitespace;
5 months ago, by wenzelm
support Isabelle fonts via patch of vscode resources;
5 months ago, by wenzelm
proper Presentation.Entity_Context for hyperlinks (amending da1108a6d249);
5 months ago, by wenzelm
clarified symbolic path;
5 months ago, by wenzelm
clarified extension name (again);
5 months ago, by wenzelm
removed obsolete material;
5 months ago, by wenzelm
update scripts, based on recent "yo code" template;
5 months ago, by wenzelm
clarified extension name (again), corresponding to qualified resources within VSCode (settings, commands, etc.);
5 months ago, by wenzelm
clarified signature;
5 months ago, by wenzelm
clarified extension name;
5 months ago, by wenzelm
clarified signature;
5 months ago, by wenzelm
clarified signature;
5 months ago, by wenzelm
clarified options;
5 months ago, by wenzelm
support local .vsix installation;
5 months ago, by wenzelm
formal record of generated package-lock.json;
5 months ago, by wenzelm
pro-forma update of version, for ongoing development;
5 months ago, by wenzelm
updated notes on Isabelle/VSCode development;
5 months ago, by wenzelm
proper engines.vscode (amending c04ccea8bdd2): required for "vsce package", e.g. via "isabelle build_vscode;
5 months ago, by wenzelm
simp rules for negative numerals
5 months ago, by haftmann
updated vscode extension: proper recoding;
5 months ago, by Fabian Huch
tuned vscode extension;
5 months ago, by Fabian Huch
tuned vscode extension: split isabelle fsp into workspace and mapping;
5 months ago, by Fabian Huch
update VSCode plugin dependencies;
5 months ago, by Fabian Huch
added Isabelle output panel to VSCode extension;
5 months ago, by Fabian Huch
Simplified a couple of extremely long and ugly apply-proofs
5 months ago, by paulson
merged
5 months ago, by wenzelm
some updates to README.md;
5 months ago, by wenzelm
refer to Isabelle settings via environment, which is provided via "isabelle vscode";
5 months ago, by wenzelm
more operations;
5 months ago, by wenzelm
more robust startup wrt. VSCode workspace (by Fabian Huch);
5 months ago, by wenzelm
various improvements to Isabelle/VSCode (by Denis Paluca and Fabian Huch);
5 months ago, by wenzelm
have Sledgehammer honor 'smt_nat_as_int' option
5 months ago, by blanchet
more handling of Zipperposition definitions in Isar proof construction
5 months ago, by blanchet
handle Zipperposition definitions in Isar proof construction
5 months ago, by blanchet
parse Zipperposition definitions
5 months ago, by blanchet
clarified URL;
5 months ago, by wenzelm
clarified pdf path;
5 months ago, by wenzelm
HTTP view of Isabelle PDF documentation;
5 months ago, by wenzelm
clarified signature;
5 months ago, by wenzelm
more robust;
5 months ago, by wenzelm
tuned message;
5 months ago, by wenzelm
clarified signature: more explicit section structure;
5 months ago, by wenzelm
clarified signature;
5 months ago, by wenzelm
clarified signature;
5 months ago, by wenzelm
tuned signature;
5 months ago, by wenzelm
tuned;
5 months ago, by wenzelm
clarified URL (again);
5 months ago, by wenzelm
more robust toplevel url: allow extra "/";
5 months ago, by wenzelm
clarified signature;
5 months ago, by wenzelm
clarified signature;
5 months ago, by wenzelm
clarified signature;
5 months ago, by wenzelm
support for PDF.js: platform-independent PDF viewer;
5 months ago, by wenzelm
more robust mime_type;
5 months ago, by wenzelm
merged
5 months ago, by wenzelm
improved support for Java Chromium Embedded Framework (JCEF): works on x86_64-linux and x86_64-windows with jdk-15 (not jdk-17), does not work on arm64 and darwin;
5 months ago, by wenzelm
one new lemma
5 months ago, by paulson
clarified options;
5 months ago, by wenzelm
clarified options;
5 months ago, by wenzelm
clarified directory;
5 months ago, by wenzelm
tuned whitespace;
5 months ago, by wenzelm
prefer strict equality, without implicit type conversion;
5 months ago, by wenzelm
tuned;
5 months ago, by wenzelm
auto-update by VSCode;
5 months ago, by wenzelm
more activationEvents, as proposed by Denis Paluca;
5 months ago, by wenzelm
tuned message;
5 months ago, by wenzelm
NEWS;
5 months ago, by wenzelm
run Isabelle/VSCode using local VSCodium installation;
5 months ago, by wenzelm
provide macos_exe, based on bin/codium from linux;
5 months ago, by wenzelm
clarified options;
5 months ago, by wenzelm
Avoid overaggresive splitting.
6 months ago, by haftmann
more lemmas for distribution
6 months ago, by haftmann
Avoid overaggresive simplification.
6 months ago, by haftmann
merged
6 months ago, by wenzelm
setup VSCode from VSCodium distribution;
6 months ago, by wenzelm
more robust package_dir, to increase chances that it works with IntelliJ IDEA;
6 months ago, by wenzelm
NEWS
6 months ago, by desharna
Mirabelle now considers goals preceding "unfolding" and "using" commands
6 months ago, by desharna
merged
6 months ago, by paulson
an assortment of new or stronger lemmas
6 months ago, by paulson
obsolete (reverting b3d6bb2ebf77): Isabelle/Naproche cache is now value-oriented;
6 months ago, by wenzelm
print outcome of Sledgehammer search in panel
6 months ago, by blanchet
print Sledgehammer error message
6 months ago, by blanchet
updated documentation to current matter of affairs
6 months ago, by haftmann
unused;
6 months ago, by wenzelm
clarified signature;
6 months ago, by wenzelm
merged
6 months ago, by desharna
added Isabelle identification to Mirabelle output
6 months ago, by desharna
uniformized fact selection for ATP and SMT in Sledgehammer
6 months ago, by desharna
provide cache for slow computations;
6 months ago, by wenzelm
used max_facts and fact_filter from slice for both ATP and SMT in sledgehammer
6 months ago, by desharna
more operations;
6 months ago, by wenzelm
more liberal parsing of Sledgehammer options to allow empty lists (as suggested by Larry Paulson)
6 months ago, by blanchet
more robust TSTP proof parsing
6 months ago, by blanchet
added possibility of extra options to SMT slices
6 months ago, by blanchet
tuned output syntax: Hoare triples are now blocks
6 months ago, by nipkow
tuned output syntax: INV and VAR are now blocks
6 months ago, by nipkow
more precise slicing computation and output when not enough lemmas are available (e.g. with the 'only' syntax 'sledgehammer (lem1 lem2 lem3)')
6 months ago, by blanchet
enable induction in one of Zipperposition's slices
6 months ago, by blanchet
made sorting of Vampire facts more robust in the face of names that deviate from the standard scheme
6 months ago, by blanchet
robustly handle empty proof blocks in Isar proof output
6 months ago, by blanchet
propagate right result when enough proofs have been found
6 months ago, by blanchet
correctly parse E proofs that assume '=' and '!=' bind more tightly than connectives
6 months ago, by blanchet
don't lose error messages
6 months ago, by blanchet
don't pass --auto-schedule to E indiscriminately -- use it instead of 'auto' in one slice
6 months ago, by blanchet
careful with partial applications
6 months ago, by blanchet
don't perform preplaying steps if preplaying is disabled
6 months ago, by blanchet
adjust TPTP THF parser to give priority to @ over other operators, to parse Ehoh proofs
6 months ago, by blanchet
tuned punctuation
6 months ago, by blanchet
handle TPTP '!=' more gracefully in Isar proof reconstruction
6 months ago, by blanchet
guard against duplicate lines in Zipperposition proofs
6 months ago, by blanchet
tuning
6 months ago, by blanchet
tuned NEWS
6 months ago, by blanchet
compile HOL-TPTP
6 months ago, by blanchet
compile Metis_Examples
6 months ago, by blanchet
more NEWS
6 months ago, by blanchet
compile mirabelle
6 months ago, by blanchet
tweaked Auto Sledgehammer's behavior and output
6 months ago, by blanchet
updated NEWS
6 months ago, by blanchet
removed experimental prover z3_tptp
6 months ago, by blanchet
print more verbose information
6 months ago, by blanchet
run all installed provers by default
6 months ago, by blanchet
update slice options centrally
6 months ago, by blanchet
further work on new Sledgehammer slicing
6 months ago, by blanchet
tweaked verbose output
6 months ago, by blanchet
tweak padding of prover slice schedule to include all provers
6 months ago, by blanchet
implemented 'max_proofs' mechanism
6 months ago, by blanchet
document new option 'max_proofs'
6 months ago, by blanchet
crude implementation of centralized slicing
6 months ago, by blanchet
removed obscure E option
6 months ago, by blanchet
take 'induction_rules' into consideration, as well as 'max_facts' even when 'only' is set
6 months ago, by blanchet
rationalize slicing format
6 months ago, by blanchet
thread slices through
6 months ago, by blanchet
simplified 'best_slice' data structure and made minor changes to slices
6 months ago, by blanchet
changed logic of 'slice' option to 'slices'
6 months ago, by blanchet
updated documentation of 'slice' (now 'slices') option
6 months ago, by blanchet
revised Sledgehammer documentation
6 months ago, by blanchet
rationalized output for forthcoming slicing model
6 months ago, by blanchet
use same default for FO and HO provers w.r.t. induction principles, based on evaluation -- this also simplifies the code
6 months ago, by blanchet
disable slicing within ATP module (in preparation for refactoring)
6 months ago, by blanchet
disable slicing within SMT (in preparation for factoring it out)
6 months ago, by blanchet
generalized the 'slice' option towards more flexible slicing
6 months ago, by blanchet
tuned -- fewer warnings;
6 months ago, by wenzelm
Added a tiny proof
6 months ago, by paulson
Deletion of a duplicate proof
6 months ago, by paulson
useful lemma integral_less
6 months ago, by paulson
merged
6 months ago, by desharna
removed unused parameter following f9908452b282
6 months ago, by desharna
treat 'using X by meson' as 'by (meson X)' to avoid loss of polymorphism (cf. metis)
6 months ago, by blanchet
fixed dodgy intro! attributes
6 months ago, by paulson
merged
6 months ago, by desharna
optimized facts traversal in TPTP translation
6 months ago, by desharna
optimized app_op_level selection in TPTP generation
6 months ago, by desharna
tuned trivial check in mirabelle_sledgehammer
6 months ago, by desharna
renamed run_action to run in Mirabelle.action record
6 months ago, by desharna
added spying of fact filtering timing
6 months ago, by desharna
tuned mirabelle_sledgehammer output
6 months ago, by desharna
added spying to Sledgehammer
6 months ago, by desharna
proper fact filter for dummy ATPs
6 months ago, by desharna
added syping of fact filtering time to sledgehammer
6 months ago, by desharna
removed unsynchronized references in mirabelle_sledgehammer
6 months ago, by desharna
tuned mirabelle_sledgehammer to have a single call to Synchronized.change per run
6 months ago, by desharna
updated to polyml-test-15c840d48c9a;
6 months ago, by wenzelm
some updates and clarification on Assumption.export_term;
6 months ago, by wenzelm
new theorem has_integral_UN
6 months ago, by paulson
updated to jdk-17.0.2+8;
6 months ago, by wenzelm
used elapsed time instead of cpu time in Mirabelle because the latter contain cpu time of all threads
6 months ago, by desharna
NEWS
6 months ago, by desharna
added Mirabelle option "-y" for dry run
6 months ago, by desharna
tuned garbage optimization
6 months ago, by desharna
added cpu time (in ms) to Mirabelle run_action output
6 months ago, by desharna
added Mirabelle option -r to randomize the goals before selection
7 months ago, by desharna
A new lemma about inverse image
7 months ago, by paulson
proper treatment of $let variables in symbol table in Sledgehammer
7 months ago, by desharna
removed unconditional TPTP symbol declaration for undefined_bool in sledgehammer
7 months ago, by desharna
merged
7 months ago, by desharna
split option "sledgehammer_atp_dest_dir" into "sledgehammer_atp_prob_dest_dir" and "sledgehammer_atp_proof_dest_dir"
7 months ago, by desharna
proper name mangling of "undefined" constants in Sledgehammer
7 months ago, by desharna
earlier availability of lifting
7 months ago, by haftmann
more correct transfer
7 months ago, by haftmann
merged
7 months ago, by desharna
proper abstraction of function variables when instantiating induction rules in Sledgehammer
7 months ago, by desharna
added lemma asympD
7 months ago, by desharna
added lemma
7 months ago, by nipkow
Some lemmas about continuous functions with integral zero
7 months ago, by paulson
merged
7 months ago, by desharna
added lemmas wf_imp_asym, wfP_imp_asymp, and wfP_imp_irreflp
7 months ago, by desharna
removed $ite from E 2.6 in THF format
7 months ago, by desharna
New and simplified theorems
7 months ago, by paulson
merged
7 months ago, by desharna
prefixed all mirabelle_sledgehammer output lines with sledgehammer output
7 months ago, by desharna
added lemma
7 months ago, by nipkow
Tiny additions inspired by Roth development
7 months ago, by paulson
allow general command transactions with presentation;
7 months ago, by wenzelm
more operations;
7 months ago, by wenzelm
clarified signature;
7 months ago, by wenzelm
tuned signature;
7 months ago, by wenzelm
support Gradle as alternative to Maven (again);
7 months ago, by wenzelm
tuned mirabelle command-line help message
7 months ago, by desharna
updated Mirabelle documentation
7 months ago, by desharna
proper documentation for induction_rules Sledgehammer option
7 months ago, by desharna
NEWS
8 months ago, by desharna
merged
8 months ago, by desharna
used TH1 for Leo-III in sledgehammer
8 months ago, by desharna
tuned run_sledgehammer and called it directly from Mirabelle
8 months ago, by desharna
exported Sledgehammer.launch_prover and use it in Mirabelle
8 months ago, by desharna
proper filtering inf induction rules in Mirabelle
8 months ago, by desharna
added nearly_all_facts_of_context and uniformized its usage in Sledgehammer and Mirabelle
8 months ago, by desharna
tuned ATP to use is_widely_irrelevant_const
8 months ago, by desharna
added support for initialization messages to Mirabelle
8 months ago, by desharna
tuned comment
8 months ago, by blanchet
support for JSON:API;
8 months ago, by wenzelm
support for Flarum server;
8 months ago, by wenzelm
tuned whitespace;
8 months ago, by wenzelm
tuned imports;
8 months ago, by wenzelm
tuned comments;
8 months ago, by wenzelm
clarified author names;
8 months ago, by wenzelm
clarified author names;
8 months ago, by wenzelm
merged
8 months ago, by wenzelm
more accurate names;
8 months ago, by wenzelm
more standard author_info;
8 months ago, by wenzelm
clarified author info and cluster nodes;
8 months ago, by wenzelm
more data integrity: name vs. address;
8 months ago, by wenzelm
clarified signature: more operations;
8 months ago, by wenzelm
clarified signature;
8 months ago, by wenzelm
tuned;
8 months ago, by wenzelm
more data integrity: name vs. address;
8 months ago, by wenzelm
tuned comments;
8 months ago, by wenzelm
merged
8 months ago, by desharna
tuned ATP to use fold_index
8 months ago, by desharna
tuned sledgehammer to use map_index
8 months ago, by desharna
merged
8 months ago, by wenzelm
more data integrity: name vs. address;
8 months ago, by wenzelm
misc tuning and clarification;
8 months ago, by wenzelm
clarified name;
8 months ago, by wenzelm
more mailing list content;
8 months ago, by wenzelm
more mailing list content;
8 months ago, by wenzelm
updated links;
8 months ago, by wenzelm
added Apache Commons Lang + Text: not particularly exciting, but provides useful things like org.apache.commons.text.StringEscapeUtils or org.apache.commons.text.diff;
8 months ago, by wenzelm
tuned ATP to use map_index
8 months ago, by desharna
removed obsolete RC tags;
8 months ago, by wenzelm
proper path;
8 months ago, by wenzelm
merged, resolving conflict in src/Doc/Implementation/Logic.thy;
8 months ago, by wenzelm
Added tag Isabelle2021-1 for changeset c2a2be496f35
8 months ago, by wenzelm
tuned;
Isabelle2021-1
8 months ago, by wenzelm
proper ML types (amending 1aa92bc4d356);
8 months ago, by wenzelm
proper types for Scala.Fun instances (amending 1aa92bc4d356);
8 months ago, by wenzelm
proper syntax category;
8 months ago, by wenzelm
provide component naproche-20211211;
8 months ago, by wenzelm
less
more
|
(0)
-30000
-10000
-3000
-1000
-960
tip