Mercurial
Mercurial
>
repos
>
isabelle
/ graph
summary
|
shortlog
|
changelog
| graph |
tags
|
bookmarks
|
branches
|
files
|
gz
|
help
less
more
|
(0)
-30000
-10000
-1920
+1920
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.
provide missing LaTeX macro, e.g. for AFP/PAC_Checker;
19 months ago, by wenzelm
clarified signature;
19 months ago, by wenzelm
streamlined division on polynomials
19 months ago, by haftmann
streamlined division on polynomials
19 months ago, by haftmann
clarified signature: re-use store/cache from build results;
19 months ago, by wenzelm
tuned signature;
19 months ago, by wenzelm
clarified signature: persistent Node.source / Snapshot.source;
19 months ago, by wenzelm
more examples;
19 months ago, by wenzelm
proper filter (amending fb4215da4919);
19 months ago, by wenzelm
clarified conditions: no_build is ok for presentation if "all_current" holds;
19 months ago, by wenzelm
tuned;
19 months ago, by wenzelm
tuned signature;
19 months ago, by wenzelm
clarified presentation_sessions: work with partial results;
19 months ago, by wenzelm
tuned signature: removed unused operations;
19 months ago, by wenzelm
tuned;
19 months ago, by wenzelm
tuned comments;
19 months ago, by wenzelm
streamlined division on polynomials
19 months ago, by haftmann
clarified packaging;
19 months ago, by wenzelm
merged
19 months ago, by wenzelm
Added tag Isabelle2022-RC2 for changeset 778152d51e97
19 months ago, by wenzelm
show SSH options in PIDE GUI;
19 months ago, by wenzelm
inplace update: proper Linux version;
19 months ago, by wenzelm
provide naproche-20220917;
19 months ago, by wenzelm
clarified NEWS;
19 months ago, by wenzelm
proper platform directory x86_64-linux, to have it purged for other platforms;
19 months ago, by wenzelm
MLton component for x86_64-linux;
19 months ago, by wenzelm
clarified Docker base image;
19 months ago, by wenzelm
proper file headers;
19 months ago, by wenzelm
tuned messages;
19 months ago, by wenzelm
support for ISABELLE_MLTON_OPTIONS, notably for Ubuntu 22.04 with external mlton executable;
19 months ago, by wenzelm
omit menu for unfinished tool;
19 months ago, by wenzelm
include ssh + rsync as required for Isabelle tools, e.g. "isabelle sync";
19 months ago, by wenzelm
more robust: snap version of docker cannot access /tmp;
19 months ago, by wenzelm
tuned signature;
19 months ago, by wenzelm
update to scala-3.2.0;
19 months ago, by wenzelm
avoid crash of JLine on Windows;
19 months ago, by wenzelm
update to jdk-17.0.4.1+1 from 22-Aug-2022 (https://docs.azul.com/core/zulu-openjdk/release-notes/11.58-17.36-august-2022);
19 months ago, by wenzelm
clarified default, following 8b695e59db3f;
19 months ago, by wenzelm
tuned signature;
19 months ago, by wenzelm
tuned;
19 months ago, by wenzelm
clarified modules;
19 months ago, by wenzelm
discontinued pointless SSH.Target: OpenSSH client can handle user@host directly;
19 months ago, by wenzelm
clarified options;
19 months ago, by wenzelm
clarified options;
19 months ago, by wenzelm
discontinued unclear timeout (stemming from jEdit JSch setup, see 14782d58a503), to make it work with native Windows ssh.exe;
19 months ago, by wenzelm
proper time values in seconds;
19 months ago, by wenzelm
clarified run_sftp: avoid platform_path via careful use of tmp_dir, to support both Windows and Cygwin ssh;
19 months ago, by wenzelm
more robust, notably for macOS (see also ff92d6edff2c);
19 months ago, by wenzelm
back to plain /tmp (despite 1df53737c59b): relevant for ssh on macOS, to avoid error "unix_listener: path too long for Unix domain socket";
19 months ago, by wenzelm
tuned names;
19 months ago, by wenzelm
proper order of platforms, to make it work uniformly on all plaform families;
19 months ago, by wenzelm
more portable;
19 months ago, by wenzelm
build both arm64-darwin and x86_64-darwin on Apple ARM hardware;
19 months ago, by wenzelm
unused;
19 months ago, by wenzelm
tuned message;
19 months ago, by wenzelm
more items;
19 months ago, by wenzelm
more robust: do not assume Bash syntax while testing for it;
19 months ago, by wenzelm
obsolete;
19 months ago, by wenzelm
merged
19 months ago, by wenzelm
proper treatment of complex multi-line script;
19 months ago, by wenzelm
more robust;
19 months ago, by wenzelm
more robust: Bash.string operations require remote bash;
19 months ago, by wenzelm
support port forwarding without multiplexing (for the sake of Windows);
19 months ago, by wenzelm
misc tuning and clarification;
19 months ago, by wenzelm
clarified signature;
19 months ago, by wenzelm
clarified signature;
19 months ago, by wenzelm
clarified signature;
19 months ago, by wenzelm
More on division concerning gauss numbers.
19 months ago, by haftmann
more robust adhoc shell script: work with Isabelle_System.export_isabelle_identifier;
19 months ago, by wenzelm
more concise instance-specific rules on euclidean relation
19 months ago, by haftmann
merged
19 months ago, by paulson
Tidied a few more proofs
19 months ago, by paulson
merged
19 months ago, by paulson
tidied a few ugly proofs
19 months ago, by paulson
let rsync re-use ssh connection via control path;
19 months ago, by wenzelm
clarified command-line;
19 months ago, by wenzelm
clarified command-line;
19 months ago, by wenzelm
tuned signature;
19 months ago, by wenzelm
proper port for Mercurial;
19 months ago, by wenzelm
clarified default: do not override port from ssh_config, which could be different from 22;
19 months ago, by wenzelm
proper Scala expression;
19 months ago, by wenzelm
clarified signature: separate unrelated modules;
19 months ago, by wenzelm
tuned;
19 months ago, by wenzelm
obsolete;
19 months ago, by wenzelm
obsolete;
19 months ago, by wenzelm
clarified error;
19 months ago, by wenzelm
merged
19 months ago, by wenzelm
removed remains of proxy_host management: delegated to .ssh/config;
19 months ago, by wenzelm
ssh client via regular OpenSSH tools, with authentic use of .ssh/config (notably proxy configuration);
19 months ago, by wenzelm
putting together related theorems
19 months ago, by haftmann
dropped auxiliary lemma
19 months ago, by haftmann
unused;
19 months ago, by wenzelm
clarified operation: avoid perl;
19 months ago, by wenzelm
discontinued unused operations;
19 months ago, by wenzelm
clarified signature: avoid exposure of JSch types;
19 months ago, by wenzelm
clarified signature: discontinue somewhat pointless SSH.Context;
19 months ago, by wenzelm
tuned;
19 months ago, by wenzelm
proper path;
19 months ago, by wenzelm
Added tag Isabelle2022-RC1 for changeset 6308eaaa88f1
19 months ago, by wenzelm
clarified release packaging: naproche-20220910 lacks arm64-linux support (and crashes);
19 months ago, by wenzelm
more documentation of 'export_classpath' (session ROOT) and 'scala_build_generated_files' (Isar command);
19 months ago, by wenzelm
merged;
19 months ago, by wenzelm
update for release;
19 months ago, by wenzelm
more command-line options;
19 months ago, by wenzelm
less specialized euclidean relation on int
19 months ago, by haftmann
update to Isabelle2022 and Ubuntu 22.04;
19 months ago, by wenzelm
proper comment: Phabricator remains on Ubuntu 20.04, which is still required as build environment for old Mercurial 3.9.2 with Python 2;
19 months ago, by wenzelm
more operations: for testing purposes;
19 months ago, by wenzelm
provide naproche-20220910 (inactive);
19 months ago, by wenzelm
clarified directory names (e.g. for multi-platform remote execution): avoid being deleted via isabelle.Components.purge;
19 months ago, by wenzelm
unused;
19 months ago, by wenzelm
update for release;
19 months ago, by wenzelm
tuned: prefer Scala Regex operations;
19 months ago, by wenzelm
tuning and updates for release;
19 months ago, by wenzelm
NEWS;
19 months ago, by wenzelm
discontinued somewhat pointless option: Proof_Display.pretty_goal_inst should always work smoothly (and not crash unexpectedly);
19 months ago, by wenzelm
give up show_main_goal (despite 922e3f9251ac): show_goal_inst is sufficient, even for final results;
19 months ago, by wenzelm
merged
19 months ago, by wenzelm
discontinue fragile operations;
19 months ago, by wenzelm
proper context option: change of underlying Options.default will not survive PIDE "Prover.options" (e.g. change of Isabelle/jEdit plugin options);
19 months ago, by wenzelm
enable show_goal_inst by default: match failure is merely a warning (see 730638d4e37a);
19 months ago, by wenzelm
updated documentation;
19 months ago, by wenzelm
support multiple sessions, with cumulative errors;
19 months ago, by wenzelm
support regex patterns on messages;
19 months ago, by wenzelm
support Pretty.unformatted, similar to ML version;
19 months ago, by wenzelm
removed odd TODO item (see 3391a493f39a);
19 months ago, by wenzelm
tuned signature;
19 months ago, by wenzelm
tuned output: more Pretty.item;
19 months ago, by wenzelm
tuned signature;
19 months ago, by wenzelm
clarified failure: warning for logical error, exception for program breakdown;
19 months ago, by wenzelm
print goal instantiation for global qed (and variations);
19 months ago, by wenzelm
clarified output;
19 months ago, by wenzelm
more robust: capture corner case seen in line 631 of "$AFP/Automatic_Refinement/Autoref_Bindings_HOL.thy" (AFP/6c87f24bb773);
19 months ago, by wenzelm
clarified message channel for 'print_state' (NB: the command was originally for TTY or Proof General);
19 months ago, by wenzelm
updated to postgresql-42.5.0;
19 months ago, by wenzelm
tool to build Isabelle component for PostgreSQL JDBC;
19 months ago, by wenzelm
clarified goal structure with proper instantiation of main goal, to support "show_goal_inst";
19 months ago, by wenzelm
option "show_states" for more verbosity of batch-builds;
19 months ago, by wenzelm
tuned --- avoid warnings;
19 months ago, by wenzelm
proper antiquotations;
19 months ago, by wenzelm
inline markup for Output.state (in contrast to c94bba7906d2): make messages available via Rendering.text_messages and thus "isabelle log" (see cb0c407fbc6e), while Rendering.output_messages of Isabelle/jEdit/VSCode is unaffected;
19 months ago, by wenzelm
proper antiquotations;
19 months ago, by wenzelm
clarified options, following e.g. "show_consts";
19 months ago, by wenzelm
proper Envir.subst operations: env is already normalized, using Envir.norm may lead to non-termination;
19 months ago, by wenzelm
unused (see 15758fced053);
19 months ago, by wenzelm
clarified modules;
19 months ago, by wenzelm
show goal instantiation, notably for 'schematic_goal' command (inactive by default);
19 months ago, by wenzelm
proper umlauts;
19 months ago, by wenzelm
tuned signature;
19 months ago, by wenzelm
tuned signature;
19 months ago, by wenzelm
tuned;
19 months ago, by wenzelm
tuned;
19 months ago, by wenzelm
tuned error message;
19 months ago, by wenzelm
merged
19 months ago, by desharna
merged
19 months ago, by desharna
moved antimono to Fun and redefined it as an abbreviation
22 months ago, by desharna
moved mono and strict_mono to Fun and redefined them as abbreviations
22 months ago, by desharna
clarified generic euclidean relation
19 months ago, by haftmann
added a bound in SMT on the number of schematic constants considered -- the code (in for_schematics) is exponential in that number
19 months ago, by blanchet
tuned signature;
19 months ago, by wenzelm
check imports more strictly, e.g. reject ".../Pure" or ".../HOL-Library.Multiset";
19 months ago, by wenzelm
tuned signature;
19 months ago, by wenzelm
tuned --- more robust syntax;
19 months ago, by wenzelm
tuned signature;
19 months ago, by wenzelm
back to more traditional import_name (reverting cceb10dcc9f9), e.g. relevant for "isabelle jedit -l CTT src/CTT/ex/Elimination.thy" to produce proper error "Cannot update finished theory CTT.Elimination";
19 months ago, by wenzelm
unused (see 347ed6219dab);
19 months ago, by wenzelm
tuned signature;
19 months ago, by wenzelm
more CONTRIBUTORS + NEWS;
19 months ago, by wenzelm
tuned;
19 months ago, by wenzelm
proper description;
19 months ago, by wenzelm
tuned whitespace;
19 months ago, by wenzelm
option "sort_updates" for record update simproc. Make proper record simproc definitions.
2022-03-07, by Norbert Schirmer
Merge
19 months ago, by paulson
Three new theorems about real polynomial functions
19 months ago, by paulson
tuned GUI;
20 months ago, by wenzelm
tuned;
20 months ago, by wenzelm
clarified GUI behaviour;
20 months ago, by wenzelm
eliminated odd Unicode blanks;
20 months ago, by wenzelm
tuned whitespace;
20 months ago, by wenzelm
eliminated DOS line endings;
20 months ago, by wenzelm
eliminated tabs, assuming tab-width=8;
20 months ago, by wenzelm
eliminated tabs, assuming tab-width=4;
20 months ago, by wenzelm
updated to current Cygwin, near 3.3.5-1;
20 months ago, by wenzelm
test macOS 12 Monterey via laramac01;
20 months ago, by wenzelm
clarified GUI update;
20 months ago, by wenzelm
clarified signature;
20 months ago, by wenzelm
tuned signature;
20 months ago, by wenzelm
more GUI functionality;
20 months ago, by wenzelm
clarified signature;
20 months ago, by wenzelm
clarified component structure, concerning initialization order;
20 months ago, by wenzelm
update VSCodium 1.65.2 ~> 1.70.1, Electron 13.5.2 ~> 18.3.5, Node.js v14.16.0 ~> v16.13.2;
20 months ago, by wenzelm
provide cvc5-1.0.2 (inactive);
20 months ago, by wenzelm
tuned output;
20 months ago, by wenzelm
tool to build Isabelle component for cvc5;
20 months ago, by wenzelm
tuned: avoid odd stateful programming;
20 months ago, by wenzelm
more markup (for batch build);
20 months ago, by wenzelm
tuned;
20 months ago, by wenzelm
tuned;
20 months ago, by wenzelm
tuned;
20 months ago, by wenzelm
more NEWS;
20 months ago, by wenzelm
updated some links;
20 months ago, by wenzelm
more links, for files that formally belong to this session;
20 months ago, by wenzelm
more links;
20 months ago, by wenzelm
tuned antiquotations;
20 months ago, by wenzelm
ZF belongs to chapter FOL, following lib/html/library_index_content.template (i.e. "Documentation" area on website);
20 months ago, by wenzelm
include groups from 'chapter_definition' in session info, based on the state of chapter_defs after processing all ROOT files (thus the declaration order does not matter);
20 months ago, by wenzelm
proper chapter_definition to prevent odd definitions by users;
20 months ago, by wenzelm
tuned;
20 months ago, by wenzelm
tuned signature;
20 months ago, by wenzelm
proper order;
20 months ago, by wenzelm
tuned whitespace for presentation;
20 months ago, by wenzelm
clarified signature of Sessions.Session: chapter_defs: vs. known_chapters (in declaration order) vs. chapters (covered by visible sessions);
20 months ago, by wenzelm
clarified syntax: more uniform;
20 months ago, by wenzelm
more robust, more strict;
20 months ago, by wenzelm
tuned signature;
20 months ago, by wenzelm
tuned;
20 months ago, by wenzelm
tuned output;
20 months ago, by wenzelm
merged
20 months ago, by wenzelm
clarified chapters: de-emphasize minor examples;
20 months ago, by wenzelm
tuned signature;
20 months ago, by wenzelm
clarified signature;
20 months ago, by wenzelm
produce root index based on sessions_structure.chapter_defs;
20 months ago, by wenzelm
provide chapter descriptions, based on lib/html/library_index_content.template;
20 months ago, by wenzelm
more robust: proper system_name;
20 months ago, by wenzelm
support 'chapter_definition' with description for presentation purposes;
20 months ago, by wenzelm
tuned whitespace;
20 months ago, by wenzelm
tuned signature;
20 months ago, by wenzelm
removed unused "def_theory" markup (stemming from be49c660ebbf), superseded e.g. by Document_Info.theory_by_file();
20 months ago, by wenzelm
more aggressive clean_directory(session_dir), while rm_tree is guarded by check_directory, i.e. it is presumably "owned" by Browser_Info.build_session();
20 months ago, by wenzelm
clarified signature;
20 months ago, by wenzelm
tuned signature;
20 months ago, by wenzelm
clarified signature;
20 months ago, by wenzelm
tuned whitespace;
20 months ago, by wenzelm
more robust: ensure that chapter/session/theory do not contain special notation (like "/" or "..");
20 months ago, by wenzelm
merged
20 months ago, by paulson
NEWS about Sum_of_Powers
20 months ago, by paulson
Removal of a duplicate theory, since that material and more is in the AFP: https://www.isa-afp.org/entries/Bernoulli.html
20 months ago, by paulson
NEWS;
20 months ago, by wenzelm
read full sessions_requirements, for more complete entity hyperlinks;
20 months ago, by wenzelm
more accurate management of dependencies: change of build_uuid causes output of HTML, but already existing/current HTML is not produced again;
20 months ago, by wenzelm
tuned signature: more general operations;
20 months ago, by wenzelm
tuned: avoid premature File.read;
20 months ago, by wenzelm
tuned signature: build_log db is specific to PostgreSQL;
20 months ago, by wenzelm
maintain "uuid" column in session build database, to identity the original build process uniquely;
20 months ago, by wenzelm
tuned signature;
20 months ago, by wenzelm
unused (amending 3d723062dc70);
20 months ago, by wenzelm
more readable string literals;
20 months ago, by wenzelm
avoid duplicate fact error on global_interpretation of residues
20 months ago, by haftmann
avoid looping simplification for z2
20 months ago, by haftmann
more formal meta data, within ".browser_info";
20 months ago, by wenzelm
tuned signature;
20 months ago, by wenzelm
support for pretty-printing of JSON trees;
20 months ago, by wenzelm
tuned signature;
20 months ago, by wenzelm
tuned: slightly more generic operations;
20 months ago, by wenzelm
remove duplicate parsing for alethe; fix skolemization;
20 months ago, by Mathias Fleury
Gauss numbers
20 months ago, by haftmann
disable laramac01 for now: system update pending;
20 months ago, by wenzelm
clarified synchronized operations: approximate file-system transactions;
20 months ago, by wenzelm
more robust concurrency: use shared Browser_Info.Context with synchronized file-system operations;
20 months ago, by wenzelm
NEWS;
20 months ago, by wenzelm
tuned;
20 months ago, by wenzelm
tuned comments, following "isabelle build" usage;
20 months ago, by wenzelm
clarified names;
20 months ago, by wenzelm
clarified modules;
20 months ago, by wenzelm
proper theory_dir for links to other session;
20 months ago, by wenzelm
tuned sources and comments;
20 months ago, by wenzelm
clarified signature;
20 months ago, by wenzelm
tuned sources and comments;
20 months ago, by wenzelm
clarified names: Browser_Info.Config vs. Browser_Info.Context;
20 months ago, by wenzelm
clarified modules;
20 months ago, by wenzelm
clarified signature: terminology of "base" (here) vs. "root" (there);
20 months ago, by wenzelm
tuned;
20 months ago, by wenzelm
proper fonts_prefix (amending c14409948063): default is "" due to self-cancellation of dir;
20 months ago, by wenzelm
streamlined
20 months ago, by haftmann
simplified computation algorithm construction
20 months ago, by haftmann
merged;
20 months ago, by wenzelm
more robust GUI initialization (amending 29441f2bfe81);
20 months ago, by wenzelm
clarified signature: just one common operation;
20 months ago, by wenzelm
clarified paths and links;
20 months ago, by wenzelm
more concise output of files: just one round;
20 months ago, by wenzelm
more robust;
20 months ago, by wenzelm
proper node_dir within presentation_dir, not source file directory;
20 months ago, by wenzelm
clarified modules;
20 months ago, by wenzelm
clarified names;
20 months ago, by wenzelm
more thorough checks of browser_info file conflicts;
20 months ago, by wenzelm
tuned;
20 months ago, by wenzelm
prefer strict operations with explicit errors (instead of missing HTML output);
20 months ago, by wenzelm
more thorough check, without path name artifacts (e.g. "./README");
20 months ago, by wenzelm
tuned signature;
20 months ago, by wenzelm
clarified signature: Sessions.Base_Info follows Sessions.Base;
20 months ago, by wenzelm
clarified signature: follow Sessions.Deps.check_errors (despite Process_Result.check);
20 months ago, by wenzelm
tuned;
20 months ago, by wenzelm
tuned whitespace;
20 months ago, by wenzelm
evade clash with index.html (allow "Index.thy" even on case-insensitive file-systems);
20 months ago, by wenzelm
discontinued special support for README.html (which was hardly ever used in the past 2 decades);
20 months ago, by wenzelm
clarified directory layout (again): mimic original directory layout, notably ISABELLE_HOME;
20 months ago, by wenzelm
more robust treatment of Document.Node.Name, following stored data;
20 months ago, by wenzelm
more robust;
20 months ago, by wenzelm
clarified directory layout: files are relative to enclosing theory;
20 months ago, by wenzelm
tuned signature: avoid duplication;
20 months ago, by wenzelm
more robust: theories could have been suppressed via option "condition";
20 months ago, by wenzelm
tuned signature;
20 months ago, by wenzelm
tuned messages (again, see d50c2129e73a): presentation setup could fail initially for take some time;
20 months ago, by wenzelm
clarified modules;
20 months ago, by wenzelm
clarified signature: support for adhoc file types;
20 months ago, by wenzelm
clarified Presentation.Nodes, with explicit Nodes.Session and Nodes.Theory;
20 months ago, by wenzelm
export entity file position as well, e.g. relevant for HTML presentation with aux. files;
20 months ago, by wenzelm
proper permissive = true (amending 475fedc02737)
20 months ago, by wenzelm
tuned signature;
20 months ago, by wenzelm
clarified signature;
20 months ago, by wenzelm
clarified signature;
20 months ago, by wenzelm
more robust directory structure: always relative to session_dir;
20 months ago, by wenzelm
discontinued slightly odd integrity check (from af2d0e07493b): requires a different approach;
20 months ago, by wenzelm
clarified signature;
20 months ago, by wenzelm
misc tuning and clarification;
20 months ago, by wenzelm
unused;
20 months ago, by wenzelm
tuned signature;
20 months ago, by wenzelm
tuned signature;
20 months ago, by wenzelm
tuned signature;
20 months ago, by wenzelm
clarified modules;
20 months ago, by wenzelm
clarified modules;
20 months ago, by wenzelm
unused;
20 months ago, by wenzelm
tuned signature;
20 months ago, by wenzelm
clarified signature: replaced Sessions.Deps by Sessions.Structure from HTML_Context;
20 months ago, by wenzelm
tuned;
20 months ago, by wenzelm
clarified signature: avoid constants from Sessions.Structure within Session.Base;
20 months ago, by wenzelm
clarified signature: avoid object-oriented HTML_Context;
20 months ago, by wenzelm
tuned type signature
20 months ago, by haftmann
tuned type signature
20 months ago, by haftmann
streamlined theorems
20 months ago, by haftmann
more thorough split rules for div and mod on numerals, tuned split rules setup
20 months ago, by haftmann
streamlined simpset building, avoiding duplicated rewrite rules
20 months ago, by haftmann
consolidated attribute name
20 months ago, by haftmann
streamlined theorems
20 months ago, by haftmann
streamlined theorems and sections
20 months ago, by haftmann
streamlined primitive definitions for integer division
20 months ago, by haftmann
reintroduced SPASS to the mix
20 months ago, by blanchet
tweaked generation of Isar proofs
20 months ago, by blanchet
tweak Sledgehammer's slicing mechanism -- updated Zipperposition's slices and make them half as long as other provers' to pack more of them in 30 s
20 months ago, by blanchet
tuned comments;
20 months ago, by wenzelm
updated to sumatra_pdf-3.4.6;
20 months ago, by wenzelm
proper Java/Scala compiler classpath (amending b42e20adaeed): ISABELLE_SETUP_CLASSPATH must not be included prematurely (breaks on Windows), instead use runtime Classpath().jars;
20 months ago, by wenzelm
revived 'try0' and 'smart' Isar proofs in Sledgehammer
20 months ago, by blanchet
Cleanup of NonstandardAnalysis
20 months ago, by paulson
A bit of cleaning up
20 months ago, by paulson
The same, without adding a new simprule
20 months ago, by paulson
moved some material from Sum_of_Powers
20 months ago, by paulson
merged
20 months ago, by wenzelm
clarified signature;
20 months ago, by wenzelm
clarified theory_names with exported content;
20 months ago, by wenzelm
proper export theory_names: theory/parents are not necessarily present (amending 4d27b520622a);
20 months ago, by wenzelm
proper treatment of empty lines (amending 08f89f0e8a62);
20 months ago, by wenzelm
clarified signature: avoid confusing operation name (amending 8cf14d4ebec4);
20 months ago, by wenzelm
merged
20 months ago, by paulson
The right way to formulate card_UNION, plus the old version for compatibility
20 months ago, by paulson
tuned comments;
20 months ago, by wenzelm
tuned signature;
20 months ago, by wenzelm
clarified signature;
20 months ago, by wenzelm
clarified signature;
20 months ago, by wenzelm
clarified signature;
20 months ago, by wenzelm
unused;
20 months ago, by wenzelm
clarified modules;
20 months ago, by wenzelm
clarified signature;
20 months ago, by wenzelm
clarified signature: more explicit types;
20 months ago, by wenzelm
clarified signature --- avoid dependent types;
20 months ago, by wenzelm
tuned whitespace;
20 months ago, by wenzelm
clarified signature: avoid public representation;
20 months ago, by wenzelm
tuned signature;
20 months ago, by wenzelm
clarified signature;
20 months ago, by wenzelm
unused;
20 months ago, by wenzelm
more accurate treatment of option "editor_output_state", e.g. when changed via Isabelle/jEdit Plugin Options panel;
20 months ago, by wenzelm
clarified signature: more explicit types;
20 months ago, by wenzelm
tuned whitespace;
20 months ago, by wenzelm
tuned, following 298707451ec2;
20 months ago, by wenzelm
unused;
20 months ago, by wenzelm
tuned, following hints by IntelliJ IDEA;
20 months ago, by wenzelm
clarified signature: more explicit types;
20 months ago, by wenzelm
tuned whitespace;
20 months ago, by wenzelm
tuned, following hints by IntelliJ IDEA;
20 months ago, by wenzelm
merged
20 months ago, by wenzelm
more GUI elements;
20 months ago, by wenzelm
clarified signature;
20 months ago, by wenzelm
tuned;
20 months ago, by wenzelm
tuned, following hints by IntelliJ IDEA;
20 months ago, by wenzelm
clarified signature --- more operations;
20 months ago, by wenzelm
clarified signature --- simplified types;
20 months ago, by wenzelm
tuned signature;
20 months ago, by wenzelm
proper toString for Content_XML, which is not covered by trait Content;
20 months ago, by wenzelm
clarified output;
20 months ago, by wenzelm
clarified signature: support different document_session, e.g. within running PIDE session;
20 months ago, by wenzelm
unused (despite cf52379c0776);
20 months ago, by wenzelm
tuned, following hints by IntelliJ IDEA;
20 months ago, by wenzelm
unused (see 696819fe2424);
20 months ago, by wenzelm
clarified signature;
20 months ago, by wenzelm
basic setup for document build panel;
20 months ago, by wenzelm
tuned, following hints by IntelliJ IDEA;
20 months ago, by wenzelm
tuned, following hints by IntelliJ IDEA;
20 months ago, by wenzelm
tuned;
20 months ago, by wenzelm
clarified signature;
20 months ago, by wenzelm
tuned, following hints by IntelliJ IDEA;
20 months ago, by wenzelm
tuned, following hints by IntelliJ IDEA;
20 months ago, by wenzelm
tuned signature;
20 months ago, by wenzelm
tuned signature;
20 months ago, by wenzelm
tuned signature, following hints by IntelliJ IDEA;
20 months ago, by wenzelm
added support for cvc5 (whose interface is almost identical to CVC4)
20 months ago, by blanchet
removing the [simp] attribute breaks too many AFP entries severely
20 months ago, by nipkow
nlists is picked up automatically but conflicts with the RBT setup
20 months ago, by nipkow
new lemma
20 months ago, by nipkow
merged
20 months ago, by nipkow
New theory of fixed length lists
20 months ago, by nipkow
Further streamlining of quick-and-dirty evaluation.
20 months ago, by haftmann
more correct approximation (contributed by Achim Brucker)
21 months ago, by Achim D. Brucker
Added tag Isabelle2022-RC0 for changeset b42e20adaeed
20 months ago, by wenzelm
proper Java/Scala compiler classpath for standalone application (see also make_isabelle_app() in Pure/Admin/build_release.scala);
20 months ago, by wenzelm
clarified message;
20 months ago, by wenzelm
provide naproche-20220808 (inactive);
20 months ago, by wenzelm
more robust data representation: notably for Store.read_session_timing with database_server;
20 months ago, by wenzelm
tuned message;
20 months ago, by wenzelm
afford default cache policy, despite 6a29709906c6;
20 months ago, by wenzelm
tuned signature;
20 months ago, by wenzelm
clarified signature: more uniform treatment of cache for Export.read_session vs. Export.read_theory;
20 months ago, by wenzelm
tuned;
20 months ago, by wenzelm
tuned signature;
20 months ago, by wenzelm
clarified signature;
20 months ago, by wenzelm
clarified modules;
20 months ago, by wenzelm
merged
20 months ago, by wenzelm
tuned;
20 months ago, by wenzelm
clarified message;
20 months ago, by wenzelm
clarified signature: prefer Export.Session_Context over Sessions.Database_Context;
20 months ago, by wenzelm
clarified signature: prefer Export.Context;
20 months ago, by wenzelm
clarified signature: find session_database within Session_Context.db_hierarchy;
20 months ago, by wenzelm
clarified signature: prefer Export.Session_Context;
20 months ago, by wenzelm
prefer Export.Context/Session_Context/Theory_Context over Sessions.Database_Context;
20 months ago, by wenzelm
clarified signature;
20 months ago, by wenzelm
tuned signature, following hints by IntelliJ IDEA;
20 months ago, by wenzelm
clarified signature: more robust treatment of server;
20 months ago, by wenzelm
discontinued Export.Provider in favour of Export.Context and its derivatives;
20 months ago, by wenzelm
clarified signature: less redundant -- Sessions.Base_Info already specifies the main session;
20 months ago, by wenzelm
tuned signature: more operations;
20 months ago, by wenzelm
misc tuning and clarification;
20 months ago, by wenzelm
clarified Document.Snapshot.all_exports: refer to material from this (virtual) session;
20 months ago, by wenzelm
clarified database query: refer to semantic theories;
20 months ago, by wenzelm
clarified signature: more operations;
20 months ago, by wenzelm
clarified signature: persistent theory_names in lexical order;
20 months ago, by wenzelm
proper session_databases for database_server: need to follow precise session_hierarchy;
20 months ago, by wenzelm
redundant;
20 months ago, by wenzelm
clarified signature: more robust close operation;
20 months ago, by wenzelm
more uniform exports: proper encoding of empty parents for Pure;
20 months ago, by wenzelm
clarified signature: more uniform treatment of empty exports;
20 months ago, by wenzelm
clarified session name: treat PIDE session as Sessions.DRAFT with imports from other sessions;
20 months ago, by wenzelm
more robust build_hierarchy: support Resources.empty / Sessions.Structure.empty (required for Build_Job.print_log);
20 months ago, by wenzelm
clarified context for retrieval: more explicit types, with optional close() operation;
20 months ago, by wenzelm
tuned;
20 months ago, by wenzelm
unused;
20 months ago, by wenzelm
retrieve information about used files;
20 months ago, by wenzelm
tuned signature -- more robust;
20 months ago, by wenzelm
tuned signature;
20 months ago, by wenzelm
clarified signature: Export.Provider knows its (accidental) theory_names;
20 months ago, by wenzelm
clarified signature;
20 months ago, by wenzelm
tuned, following hints by IntelliJ IDEA;
20 months ago, by wenzelm
clarified signature: proper session_name for Sessions.Base (like Sessions.Info);
20 months ago, by wenzelm
tuned signature;
20 months ago, by wenzelm
clarified signature;
20 months ago, by wenzelm
clarified signature;
20 months ago, by wenzelm
clarified signature;
20 months ago, by wenzelm
avoid multiple load_commands;
20 months ago, by wenzelm
avoid redundant dependencies.load_commands with potential errors (amending ea4f86914cb2);
20 months ago, by wenzelm
tuned signature -- avoid redundant arguments;
20 months ago, by wenzelm
tuned -- following hints by IntelliJ IDEA;
20 months ago, by wenzelm
tuned signature;
20 months ago, by wenzelm
tuned comments;
20 months ago, by wenzelm
removed somewhat pointless transaction: db is meant to be finished (or updated monotonically);
20 months ago, by wenzelm
tuned signature;
20 months ago, by wenzelm
clarified signature;
20 months ago, by wenzelm
clarified signature: avoid repeated db_context.input_database;
20 months ago, by wenzelm
clarified signature: more robust;
20 months ago, by wenzelm
removed somewhat pointless operations (see a6c69599ab99);
21 months ago, by wenzelm
clarified signature;
21 months ago, by wenzelm
tuned;
21 months ago, by wenzelm
tuned;
21 months ago, by wenzelm
clarified signature;
21 months ago, by wenzelm
clarified names;
21 months ago, by wenzelm
clarified signature;
21 months ago, by wenzelm
clarified names;
21 months ago, by wenzelm
clarified signature;
21 months ago, by wenzelm
clarified signature: more explicit types;
21 months ago, by wenzelm
unused (see 0d30ea76756c);
21 months ago, by wenzelm
tuned;
21 months ago, by wenzelm
clarified signature;
21 months ago, by wenzelm
tuned;
21 months ago, by wenzelm
unused (see 3064e165c660);
21 months ago, by wenzelm
merge
20 months ago, by blanchet
changed the order of Zipperposition slices in Sledgehammer
20 months ago, by blanchet
merged
20 months ago, by paulson
The wellordering instantiation for length-ordered lists
20 months ago, by paulson
show sum_list defn
20 months ago, by nipkow
prettified def
21 months ago, by nipkow
More lemmas.
21 months ago, by haftmann
Some more proofs.
21 months ago, by haftmann
a few new theorems
21 months ago, by paulson
tuned;
21 months ago, by wenzelm
clarified while-loops;
21 months ago, by wenzelm
updated to postgresql-42.4.0;
21 months ago, by wenzelm
updated to flatlaf-2.4;
21 months ago, by wenzelm
updated to pdfjs-2.14.305;
21 months ago, by wenzelm
more robust: retain Classpath value;
21 months ago, by wenzelm
tuned;
21 months ago, by wenzelm
mor robust;
21 months ago, by wenzelm
clarified modules;
21 months ago, by wenzelm
clarified signature;
21 months ago, by wenzelm
update documentation, following 21c1f82e7f5d;
21 months ago, by wenzelm
proper classpath for Scala compiler invocation (amending 14e22b525b13);
21 months ago, by wenzelm
merged
21 months ago, by wenzelm
support for dynamic classpath from exports;
21 months ago, by wenzelm
clarified signature;
21 months ago, by wenzelm
tuned signature;
21 months ago, by wenzelm
Avoid shadowing original List._ namespace.
21 months ago, by haftmann
replaced complicated lemma by a simpler one
21 months ago, by nipkow
clarified signature;
21 months ago, by wenzelm
clarified modules;
21 months ago, by wenzelm
merged
21 months ago, by wenzelm
more documentation;
21 months ago, by wenzelm
tuned;
21 months ago, by wenzelm
removed obsolete commands;
21 months ago, by wenzelm
command 'scala_build_generated_files' with proper management of source dependencies;
21 months ago, by wenzelm
clarified signature;
21 months ago, by wenzelm
tuned messages;
21 months ago, by wenzelm
support more file types;
21 months ago, by wenzelm
support for Java language;
21 months ago, by wenzelm
clarified signature;
21 months ago, by wenzelm
clarified signature;
21 months ago, by wenzelm
support for classpath artifacts within session structure:
21 months ago, by wenzelm
clarified names;
21 months ago, by wenzelm
clarified signature;
21 months ago, by wenzelm
clarified signature;
21 months ago, by wenzelm
clarified signature;
21 months ago, by wenzelm
clarified signature;
21 months ago, by wenzelm
unused;
21 months ago, by wenzelm
clarified signature;
21 months ago, by wenzelm
tuned signature: more explicit types;
21 months ago, by wenzelm
fix document build error
21 months ago, by Lukas Stevens
tuned (some HOL lints, by Yecine Megdiche);
21 months ago, by Fabian Huch
moved lemma fromm AFP
21 months ago, by nipkow
tuned names
21 months ago, by nipkow
refined code equations for characters
21 months ago, by haftmann
prefer non-JNI SAT solvers by default in Nitpick
21 months ago, by blanchet
milder Sledgehammer messages
21 months ago, by blanchet
moved lemmas from AFP
21 months ago, by nipkow
refined code equations for characters
21 months ago, by haftmann
tuned comments;
21 months ago, by wenzelm
support for Isabelle/Scala/Java modules in Isabelle/ML;
21 months ago, by wenzelm
more robust Scala 3 indentation, for the sake of IntelliJ IDEA;
21 months ago, by wenzelm
clarified signature: read_theory_exports is already ordered;
21 months ago, by wenzelm
clarified signature;
21 months ago, by wenzelm
tuned;
21 months ago, by wenzelm
sketch for word-specific lsb and msb
21 months ago, by haftmann
switch to Scala 3;
21 months ago, by wenzelm
minor performance tuning: avoid redundant BigInt construction;
21 months ago, by wenzelm
added lemmas total_on_trancl and totalp_on_tranclp
21 months ago, by desharna
Move code lemmas for symbolic computation of bit operations on int to distribution.
21 months ago, by haftmann
fixed diverging simproc cont_intro
21 months ago, by desharna
corrections and adjustions for Scala 3
21 months ago, by haftmann
more complete set of code equations
21 months ago, by haftmann
officical abstract characters for code generation
21 months ago, by haftmann
provide components for scala3 (still inactive);
22 months ago, by wenzelm
updated download version;
22 months ago, by wenzelm
obsolete;
22 months ago, by wenzelm
more keywords for scala3;
22 months ago, by wenzelm
discontinued Isabelle tools implemented as .scala scripts;
22 months ago, by wenzelm
tuned proofs
22 months ago, by desharna
clarified heap alignment, to make it potentially more stable on macOS;
22 months ago, by wenzelm
tuned proof
22 months ago, by desharna
added lemmas domain_comp and unify_gives_minimal_domain
22 months 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
22 months ago, by desharna
merged
22 months ago, by desharna
added definition IMGU and lemmas IMGU_iff_Idem_and_MGU and unify_computes_IMGU
22 months ago, by desharna
more macOS versions;
22 months ago, by wenzelm
prefer Isabelle/Scala operations;
22 months ago, by wenzelm
merged
22 months ago, by wenzelm
clarified IO, following Java 11 and Isabelle/Scala;
22 months ago, by wenzelm
prefer Scala operations;
22 months ago, by wenzelm
minor tuning;
22 months ago, by wenzelm
switched to statically compiled ci profile;
22 months ago, by Fabian Huch
more operations on Bytes.T;
22 months ago, by wenzelm
more operations on Bytes.T;
22 months ago, by wenzelm
tuned BNF bounds for function space and bounded sets; NEWS and CONTRIBUTORS
22 months ago, by traytel
strict bounds for BNFs (by Jan van Brügge)
22 months ago, by traytel
More lemmas.
22 months ago, by haftmann
Centralized some char-related lemmas in distribution.
22 months ago, by haftmann
prefer antiquotations;
22 months ago, by wenzelm
clarified modules;
22 months ago, by wenzelm
more documentation;
22 months ago, by wenzelm
merged
22 months ago, by wenzelm
tuned whitespace;
22 months ago, by wenzelm
clarified signature: File.read_lines is based on scalable Bytes.T;
22 months ago, by wenzelm
clarified modules;
22 months ago, by wenzelm
prefer scalable Bytes.T;
22 months ago, by wenzelm
unused;
22 months ago, by wenzelm
prefer scalable Bytes.T;
22 months ago, by wenzelm
missing recursive let-expansion in SMT translation
22 months ago, by Mathias Fleury
merged
22 months ago, by desharna
added lemma monotone_on_o
22 months ago, by desharna
redefined mono_on and strict_mono_on as an abbreviation of monotone_on
22 months ago, by desharna
changed argument order of mono_on and strict_mono_on to uniformize with monotone_on and other predicates
22 months ago, by desharna
more robust CSV syntax, e.g. for "pull_date";
22 months ago, by wenzelm
merged
22 months ago, by wenzelm
more scalable generated files and code export, using Bytes.T;
22 months ago, by wenzelm
more operations;
22 months ago, by wenzelm
proper execution of Bytes.write;
22 months ago, by wenzelm
Avoid calculations where not necessary.
22 months ago, by haftmann
Prefer existing horner sum combinator.
22 months ago, by haftmann
Executable lexords.
22 months ago, by haftmann
Less warnings.
22 months ago, by haftmann
merged
22 months ago, by wenzelm
more operations;
22 months ago, by wenzelm
removed unused operations;
22 months ago, by wenzelm
clarified signature: more operations;
22 months ago, by wenzelm
tuned;
22 months ago, by wenzelm
tuned comments;
22 months ago, by wenzelm
tuned;
22 months ago, by wenzelm
clarified session resources for bootstrap, notably for Scala functions;
22 months ago, by wenzelm
tuned;
22 months ago, by wenzelm
clarified signature;
22 months ago, by wenzelm
tuned signature;
22 months ago, by wenzelm
clarified types and defaults;
22 months ago, by wenzelm
merged
22 months ago, by desharna
added lemmas monotone{,_on}_multp_multp_image_mset
22 months ago, by desharna
added lemmas monotone_on_empty[simp] and monotone_on_subset
22 months ago, by desharna
added predicate monotone_on and redefined monotone to be an abbreviation.
22 months ago, by desharna
merged
22 months ago, by wenzelm
NEWS;
22 months ago, by wenzelm
support XZ compression in Isabelle/ML;
22 months ago, by wenzelm
prefer scalable byte strings;
22 months ago, by wenzelm
more scalable byte messages, notably for Scala functions in ML;
22 months ago, by wenzelm
tuned comments;
22 months ago, by wenzelm
clarified ML pretty printing;
22 months ago, by wenzelm
clarified signature: more operations;
22 months ago, by wenzelm
tuned signature;
22 months ago, by wenzelm
tuned comments;
22 months ago, by wenzelm
tuned signature: more operations;
22 months ago, by wenzelm
tuned signature: more operations;
22 months ago, by wenzelm
tuned signature;
22 months ago, by wenzelm
clarified signature: avoid repeated string copying via Substring.slice;
22 months ago, by wenzelm
support for scalable byte strings, with incremental construction;
22 months ago, by wenzelm
clarified signature;
22 months ago, by wenzelm
remove unused file following 51e696887b81;
22 months ago, by wenzelm
added lemma map_mono_strict_suffix
22 months ago, by desharna
more robust: always override ISABELLE_IDENTIFIER from environment;
22 months ago, by wenzelm
"isabelle vscode" is regular user-space tool;
22 months ago, by wenzelm
fix veriT reconstruction for and_pos and lambda-lifting
22 months ago, by Mathias Fleury
added lemmas image_mset_eq_{image_mset_plus,plus,plus_image_mset}D, and multp_image_mset_image_msetD
22 months ago, by desharna
clarified options of "isabelle hg_sync" vs. "isabelle sync";
22 months ago, by wenzelm
tuned layout;
22 months ago, by wenzelm
misc tuning;
22 months ago, by wenzelm
clarified document structure;
22 months ago, by wenzelm
promote "isabelle sync" to regular user-space tool, with proper documentation;
22 months ago, by wenzelm
more comments;
22 months ago, by wenzelm
more options;
22 months ago, by wenzelm
sync session images, based on accidental local state;
22 months ago, by wenzelm
more informative release_snapshot, to see better where the cronjob fails;
22 months ago, by wenzelm
more robust, notably for crontab;
22 months ago, by wenzelm
clarified names;
22 months ago, by wenzelm
tuned;
22 months ago, by wenzelm
tuned;
22 months ago, by wenzelm
proper make_port for regular situation;
22 months ago, by wenzelm
clarified types -- proper default_port via make_port;
22 months ago, by wenzelm
proper nominal_port, notably for port forwarding;
22 months ago, by wenzelm
some additional lemmas and a little tidying up
22 months ago, by paulson
merged
22 months ago, by desharna
added lemma totalp_on_total_on_eq[pred_set_conv]
22 months ago, by desharna
added lemma reflp_on_empty[simp] and totalp_on_empty[simp]
22 months ago, by desharna
removed non-standard spaces in output
22 months ago, by nipkow
merged
22 months ago, by wenzelm
avoid noise via context.progress (amending 68162e4f60a7);
22 months ago, by wenzelm
more robust treatment of rsync on macOS (see also 96fb1f9a4042);
22 months ago, by wenzelm
tuned whitespace;
22 months ago, by wenzelm
more robust: no change of directory attributes of initial test, notably target without .hg_sync meta data;
22 months ago, by wenzelm
merged
22 months ago, by desharna
added lemmas reflp_on_Inf and reflp_on_Sup
22 months ago, by desharna
replaced HOL.implies by Pure.imp in reflp_mono for consistency with other lemmas
22 months ago, by desharna
added lemmas reflp_on_inf, reflp_on_sup, and reflp_on_mono
22 months ago, by desharna
merged
22 months ago, by wenzelm
more robust: protect_args does not work with rsync 2.x from macOS, and is not required in typical situations;
22 months ago, by wenzelm
clarified context with global defaults;
22 months ago, by wenzelm
tuned signature;
22 months ago, by wenzelm
clarified signature: more explicit type Rsync.Context;
22 months ago, by wenzelm
clarified signature;
22 months ago, by wenzelm
clarified modules;
22 months ago, by wenzelm
provide python-3.10.4 for darwin and linux;
22 months ago, by Fabian Huch
provide hugo-0.88.1 for darwin and linux;
22 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);
22 months ago, by wenzelm
avoid redundant meta data: exclude .hg_archival.txt;
22 months ago, by wenzelm
clarified remote vs. local build_history: operate on hg_sync directory instead of repository;
22 months ago, by wenzelm
proper operation on String, not Path;
22 months ago, by wenzelm
clarified signature: cwd can be misleading --- changes meaning of target;
22 months ago, by wenzelm
merged
22 months ago, by wenzelm
more meta data;
22 months ago, by wenzelm
clarified signature: more operations;
22 months ago, by wenzelm
tuned messages;
22 months ago, by wenzelm
provide .hg_sync meta data;
22 months ago, by wenzelm
clarified signature;
22 months ago, by wenzelm
clarified options;
23 months ago, by wenzelm
more robust;
23 months ago, by wenzelm
clarified signature (again);
23 months ago, by wenzelm
clarified signature;
23 months ago, by wenzelm
NEWS
22 months ago, by desharna
added lemmas reflp_on_subset, totalp_on_subset, and total_on_subset
22 months ago, by desharna
introduced predicate reflp_on and redefined reflp to be an abbreviation
22 months ago, by desharna
merged
23 months ago, by nipkow
insort renamings
23 months ago, by nipkow
more operations;
23 months ago, by wenzelm
support explicit SSH port;
23 months ago, by wenzelm
redundant (after f28aee3ad1e6): self_update already takes care of currently active Isabelle clone;
23 months ago, by wenzelm
clarified options;
23 months ago, by wenzelm
Added lemmas
23 months ago, by nipkow
merged
23 months ago, by paulson
Five slightly useful lemmas
23 months ago, by paulson
clarified option -T;
23 months ago, by wenzelm
preserve jars for quick testing;
23 months ago, by wenzelm
tuned names;
23 months ago, by wenzelm
clarified documentation: $ISABELLE_HOME is not a repository for regular releases;
23 months ago, by wenzelm
clarified command-line options;
23 months ago, by wenzelm
proper anchored pattern;
23 months ago, by wenzelm
support thorough check of file content;
23 months ago, by wenzelm
more documentation;
23 months ago, by wenzelm
clarified signature;
23 months ago, by wenzelm
tuned messages;
23 months ago, by wenzelm
tuned whitespace;
23 months ago, by wenzelm
merged
23 months ago, by wenzelm
support to synchronize Isabelle + AFP repositories;
23 months ago, by wenzelm
more robust: local repository required;
23 months ago, by wenzelm
support option -r;
23 months ago, by wenzelm
omit pointless option;
23 months ago, by wenzelm
tuned;
23 months ago, by wenzelm
more documentation;
23 months ago, by wenzelm
support filter rules, notably "protect";
23 months ago, by wenzelm
support for "isabelle hg_sync";
23 months ago, by wenzelm
clarified signature;
23 months ago, by wenzelm
tuned comments;
23 months ago, by wenzelm
clarified signature;
23 months ago, by wenzelm
tuned signature;
23 months ago, by wenzelm
tuned signature;
23 months ago, by wenzelm
support rsync;
23 months ago, by wenzelm
added lemmas Multiset.bex_{least,greatest}_element
23 months ago, by desharna
added predicate totalp_on and abbreviation totalp
23 months ago, by desharna
excluded dummy ATPs from Sledgehammer's default provers
23 months ago, by desharna
move monotone from Complete_Partial_Order to Orderings
23 months ago, by desharna
qualified name to fix integrable_cong ambiguity
23 months ago, by paulson
Renamed the misleading has_field_derivative_iff_has_vector_derivative. Inserted a number of minor lemmas
23 months ago, by paulson
Eliminated two unnecessary inductions
23 months ago, by paulson
NEWS
23 months ago, by desharna
added lemma image_mset_filter_mset_swap
23 months ago, by desharna
merged
23 months ago, by desharna
added lemmas filter_mset_cong{0,}
23 months ago, by desharna
»nil« seems to be a reserved constructor word in PolyML
23 months ago, by haftmann
tidied auto / simp with null arguments
23 months ago, by paulson
tuned signature;
23 months ago, by wenzelm
provide Isabelle/Electron test;
23 months ago, by wenzelm
tuned text;
23 months ago, by wenzelm
tuned text;
23 months ago, by wenzelm
Tidied up some super-messy proofs
23 months ago, by paulson
Added a couple of obvious simprules
23 months ago, by paulson
added lemma
24 months ago, by nipkow
tuned signature: avoid problems with scala3;
2022-04-22, by wenzelm
proper indentation;
2022-04-22, by wenzelm
merged
2022-04-22, by wenzelm
clarified management of interpreter threads: more generic;
2022-04-22, by wenzelm
clarified signature;
2022-04-21, by wenzelm
clarified signature;
2022-04-21, by wenzelm
clarified signature, based on hints by IntelliJ IDEA;
2022-04-21, by wenzelm
tuned signature;
2022-04-21, by wenzelm
more robust: avoid partiality;
2022-04-09, by wenzelm
tuned;
2022-04-09, by wenzelm
clarified signature;
2022-04-09, by wenzelm
clarified signature;
2022-04-09, by wenzelm
tuned --- avoid warnings in scala3;
2022-04-09, by wenzelm
clarified signature;
2022-04-09, by wenzelm
pass new option only to new version of E
2022-04-13, by blanchet
merged
2022-04-11, by desharna
reused slice in Sledgehammer's minimizer
2022-04-09, by desharna
merged
2022-04-09, by wenzelm
revert 2c861b196d52: still required in HOL/Library/Code_Test.thy;
2022-04-09, by wenzelm
merged
2022-04-09, by wenzelm
tuned --- avoid warnings in scala3;
2022-04-09, by wenzelm
tuned --- avoid redundant patterns;
2022-04-09, by wenzelm
avoid pattern-match warnings, notably in scala3;
2022-04-09, by wenzelm
proper type conversion for scala-2.13: problem was unnoticed since ca17e9ebfdf1;
2022-04-09, by wenzelm
tuned --- accomodate scala3;
2022-04-09, by wenzelm
proper type conversion for scala-2.13: problem was unnoticed since ca17e9ebfdf1;
2022-04-09, by wenzelm
back to more ambitious scala-3.1.1 (see 8b7497992301);
2022-04-08, by wenzelm
tuned --- fewer warnings in scala3;
2022-04-08, by wenzelm
tuned -- avoid warnings for scala3;
2022-04-08, by wenzelm
tuned signature -- avoid warnings for scala3;
2022-04-08, by wenzelm
removed unused flag (see 25c6423ec538);
2022-04-08, by wenzelm
clarified versions;
2022-04-07, by wenzelm
documentation on diagnostic devices for code generation
2022-04-09, by haftmann
more correct language
2022-04-09, by haftmann
enable an E option suggested by Petar Vukmirovic
2022-04-08, by blanchet
used HTTPS for SystemOnTPTP
2022-04-07, by desharna
moved from AFP to distribution
2022-04-07, by haftmann
avoid static access to sun.tools.jconsole: more robust compilation (notably with scala3), but less robust invocation;
2022-04-06, by wenzelm
more operations;
2022-04-06, by wenzelm
clarified signature;
2022-04-06, by wenzelm
tuned: avoid ambiguity in scala3;
2022-04-04, by wenzelm
clarified signature: avoid ambiguity in scala3;
2022-04-04, by wenzelm
clarified signature: avoid ambiguity in scala3;
2022-04-04, by wenzelm
more robust types (for scala3);
2022-04-04, by wenzelm
tuned for scala3;
2022-04-04, by wenzelm
proper indentation (relevant for scala3);
2022-04-04, by wenzelm
adjusted printing of type annotations to accomodate Scala 3
2022-04-03, by haftmann
two new examples
2022-04-03, by paulson
pass constructor arity as part of case certficiate
2022-04-02, by haftmann
tuned whitespace in generated code
2022-04-02, by haftmann
tuned, centralizing case distinction at one place at the cost of modest duplication
2022-04-01, by haftmann
clarified formatting, for the sake of scala3;
2022-04-01, by wenzelm
merged
2022-04-01, by wenzelm
tuned formatting;
2022-04-01, by wenzelm
clarified formatting, for the sake of scala3;
2022-04-01, by wenzelm
tuned
2022-04-01, by haftmann
tuned
2022-04-01, by haftmann
merge
2022-04-01, by blanchet
tuned slices to get the fifth Zipperposition slice in a typical run
2022-04-01, by blanchet
merged
2022-04-01, by desharna
tuned sledgehammer documentation
2022-04-01, by desharna
tuned spelling;
2022-04-01, by wenzelm
merged
2022-04-01, by wenzelm
updated to scala-parser-combinators 2.1.0, which also fits to scala-3.0.2;
2022-04-01, by wenzelm
clarified invocation of isabelle.setup.Setup: -classpath allows multiple jars, as required for scala3;
2022-04-01, by wenzelm
tuned: eliminted do-while for the sake of scala3;
2022-03-31, by wenzelm
prefer scala 3.0.x, for option "-source 3.0-migration";
2022-03-31, by wenzelm
tuned: avoid problems with scala3;
2022-03-31, by wenzelm
tuned: avoid problems with scala3;
2022-03-31, by wenzelm
provide SCALA_INTERFACES for isabelle_setup;
2022-03-30, by wenzelm
build Isabelle Scala component from official downloads (for scala-3.1.1);
2022-03-26, by wenzelm
added documentation
2022-04-01, by desharna
merged
2022-04-01, by desharna
tuned sledehammer to return best succeeding preplay method
2022-03-31, by desharna
expanded sledgehammer's expect option with some_preplayed
2022-03-30, by desharna
added preplay results to sledgehammer_output
2022-03-29, by desharna
tuned sledgehammer to suggest (smt (verit)) on failing smt preplay for all but Z3
2022-03-31, by desharna
further tweaked E's setup
2022-03-31, by blanchet
tweaked E setup
2022-03-31, by blanchet
merged
2022-03-29, by desharna
post-merged into new Lethe code
2022-03-29, by desharna
merged
2022-03-29, by desharna
fixed generation of Isar proofs e89709b80b6e
2022-03-28, by desharna
NEWS and CONTRIBUTORS
2022-03-29, by haftmann
nicer TPTP output
2022-03-29, by blanchet
regenerated
2022-03-29, by haftmann
tighter check to ensure that patterns remain left-linear, previous implementation was overcautious
2022-03-29, by haftmann
tuned
2022-03-29, by haftmann
tuned
2022-03-29, by haftmann
separated treatment of undefined bodys
2022-03-28, by haftmann
tuned arguments
2022-03-28, by haftmann
modernized handling of variables
2022-03-28, by haftmann
structurally tuned
2022-03-27, by haftmann
tuned names
2022-03-27, by haftmann
prefer build combinator
2022-03-27, by haftmann
tuned whitespace
2022-03-27, by haftmann
proper option argument;
2022-03-25, by wenzelm
prefer Isabelle shasum over the old command-line tool with its extra marker character;
2022-03-25, by wenzelm
tuned signature;
2022-03-25, by wenzelm
tuned signature;
2022-03-25, by wenzelm
tuned text, without update of component for now;
2022-03-25, by wenzelm
omit somewhat pointless integrity check;
2022-03-25, by wenzelm
tuned;
2022-03-25, by wenzelm
compile TPTP module
2022-03-25, by blanchet
compile mirabelle
2022-03-25, by blanchet
further modernized E setup
2022-03-25, by blanchet
cleaned up obsolete E setup and a bit of SPASS
2022-03-25, by blanchet
second and last step in making time slicing more flexible in Sledgehammer: try to honor desired slice size
2022-03-25, by blanchet
first step in making time slicing more flexible in Sledgehammer: label slices with 'slice size'
2022-03-25, by blanchet
updated vscode_extension;
2022-03-25, by wenzelm
added parentheses in TPTP output -- seem necessary for some provers
2022-03-25, by blanchet
merged
2022-03-24, by wenzelm
provide pre-built vscodium-1.65.2 for all platforms;
2022-03-24, by wenzelm
tuned;
2022-03-24, by wenzelm
provide vscode_extension via component, thus users don't need Node.js development tools;
2022-03-24, by wenzelm
clarified options;
2022-03-24, by wenzelm
Some new library lemmas
2022-03-24, by paulson
merged
2022-03-24, by paulson
really removing Dedekind_real
2022-03-24, by paulson
merged
2022-03-24, by paulson
Moving Dedekind_Real to the AFP
2022-03-24, by paulson
tuned
2022-03-24, by haftmann
separated case reduction
2022-03-24, by haftmann
separated selector function entirely
2022-03-24, by haftmann
self-contained extraction auf clauses
2022-03-24, by haftmann
extracted selector function, restoring code generation for let expressions
2022-03-24, by haftmann
streamlined
2022-03-24, by haftmann
streamlined
2022-03-24, by haftmann
streamlined
2022-03-24, by haftmann
disentangled
2022-03-24, by haftmann
merged
2022-03-23, by wenzelm
tuned message;
2022-03-23, by wenzelm
more operations;
2022-03-23, by wenzelm
tuned signature;
2022-03-23, by wenzelm
more robust install/uninstall;
2022-03-23, by wenzelm
more formal extension_manifest, with shasum for sources;
2022-03-23, by wenzelm
tuned;
2022-03-23, by wenzelm
tuned signature;
2022-03-23, by wenzelm
clarified signature;
2022-03-23, by wenzelm
proper usage;
2022-03-23, by wenzelm
tuned -- follow sha1_digest in src/Tools/Setup/src/Build.java;
2022-03-22, by wenzelm
tuned signature;
2022-03-22, by wenzelm
clarified modules;
2022-03-22, by wenzelm
tuned signature;
2022-03-22, by wenzelm
... and removing Primrec from ROOT too
2022-03-23, by paulson
Removal of the Primrec example in preparation for making it an AFP entry
2022-03-23, by paulson
merged
2022-03-23, by desharna
avoided recomputation in Cooper.djf and ran `isabelle regenerate_cooper`
2022-02-23, by desharna
split veriT reconstruction into Lethe and veriTÂ part
2022-03-14, by Mathias Fleury
clarified options;
2022-03-22, by wenzelm
more robust errors -- on foreground process instead of background server;
2022-03-22, by wenzelm
clarified options -l vs. -R;
2022-03-22, by wenzelm
command-line arguments for "isabelle vscode", similar to "isabelle jedit";
2022-03-22, by wenzelm
proper command-line tool;
2022-03-22, by wenzelm
support console output, e.g. "isabelle vscode -C -- --help";
2022-03-22, by wenzelm
run Isabelle/VSCode via Scala;
2022-03-22, by wenzelm
clarified module name;
2022-03-21, by wenzelm
clean build from explicit MANIFEST: avoid accidental garbage in vsix package;
2022-03-21, by wenzelm
incorporate build_grammar into build_vscode_extension;
2022-03-21, by wenzelm
removed old generated file;
2022-03-21, by wenzelm
Tidied several ugly proofs in some elderly examples
2022-03-16, by paulson
tuned message;
2022-03-15, by wenzelm
clarified errors;
2022-03-15, by wenzelm
tuned messages;
2022-03-15, by wenzelm
support Node.js as well, reusing the engine from Electron/VSCodium;
2022-03-15, by wenzelm
updated to vscode 1.65.2;
2022-03-15, by wenzelm
proper result check;
2022-03-15, by wenzelm
merged
2022-03-14, by wenzelm
clarified directory layout and settings: more robust on all platforms;
2022-03-14, by wenzelm
tuned;
2022-03-14, by wenzelm
support Electron application framework;
2022-03-14, by wenzelm
generated lemma map_ident_strong for BNFs
2022-03-11, by desharna
updated SMT certificates
2022-03-11, by desharna
used more descriptive assert names in SMT-Lib output
2022-03-11, by desharna
clarified and unified executable names;
2022-03-12, by wenzelm
tuned;
2022-03-12, by wenzelm
tuned;
2022-03-12, by wenzelm
merged
2022-03-11, by wenzelm
suppress OCaml icons: avoid conflict of .ml and .ML, due to case-insensitive file-names in VSCode;
2022-03-11, by wenzelm
fix handling of lambdas in reconstruction of eq_congruent
2022-03-11, by Mathias Fleury
more robust: avoid breakdown of Search dialog;
2022-03-11, by wenzelm
tuned;
2022-03-11, by wenzelm
always use Isabelle encoding, as in Isabelle/jEdit;
2022-03-11, by wenzelm
tuned signature;
2022-03-11, by wenzelm
clarified signature: more uniform ts vs. Scala;
2022-03-11, by wenzelm
discontinued isabelle_filesystem (superseded by isabelle_encoding), see also da1108a6d249;
2022-03-11, by wenzelm
actually decode/encode symbols;
2022-03-10, by wenzelm
merged
2022-03-10, by wenzelm
prefer yarn over npm;
2022-03-10, by wenzelm
more accurate .hgignore;
2022-03-10, by wenzelm
clarified startup of "isabelle vscode": vscodium component is required, with patches for Isabelle/VSCode;
2022-03-10, by wenzelm
tuned messages;
2022-03-09, by wenzelm
proper init_resources for macos;
2022-03-09, by wenzelm
clarified names;
2022-03-09, by wenzelm
clarified modules: vscode vs. extension;
2022-03-09, by wenzelm
inline Isabelle symbols into source text, so that "isabelle vscode" can start up properly without access to process.env or fs;
2022-03-09, by wenzelm
more operations;
2022-03-09, by wenzelm
tuned comments;
2022-03-09, by wenzelm
patch VSCode source tree to support isabelle_encoding.ts;
2022-03-09, by wenzelm
more robust, pass "yarn valid-layers-check";
2022-03-08, by wenzelm
clarified directories;
2022-03-08, by wenzelm
patch for vscode encoding "UTF-8-Isabelle": clone of "utf8", no symbols yet;
2022-03-08, by wenzelm
fit into vscode source conventions;
2022-03-08, by wenzelm
A tiny further cleanup
2022-03-09, by paulson
Tidied some messy proofs
2022-03-09, by paulson
merged
2022-03-08, by nipkow
more count_list lemmas
2022-03-07, by nipkow
towards UTF-8-Isabelle symbol encoding;
2022-03-07, by wenzelm
updated to VSCode 1.65.0;
2022-03-07, by wenzelm
clarified char symbols: cover most European languages;
2022-03-07, by wenzelm
more elementary Symbol.Matcher without detour via Regex (see also Pure/General/symbol_explode.ML);
2022-03-07, by wenzelm
tuned comments;
2022-03-07, by wenzelm
more robust dependencies: avoid implicit update, escpecially of underlying vscode engine;
2022-03-07, by wenzelm
proper file headers;
2022-03-07, by wenzelm
added count_list lemmas
2022-03-06, by nipkow
tuned message;
2022-03-06, by wenzelm
more compact result;
2022-03-06, by wenzelm
prepare patched version more thoroughly, with explicit patches;
2022-03-06, by wenzelm
tuned signature;
2022-03-06, by wenzelm
recover platform-specific node binaries from original download, notably for node-pty for Terminal;
2022-03-05, by wenzelm
tuned message;
2022-03-05, by wenzelm
tuned;
2022-03-05, by wenzelm
tuned imports;
2022-03-05, by wenzelm
misc tuning and clarification;
2022-03-05, by wenzelm
more executable files;
2022-03-05, by wenzelm
tuned;
2022-03-05, by wenzelm
tuned output;
2022-03-05, by wenzelm
clarified signature;
2022-03-05, by wenzelm
tuned, based on suggestions by IntelliJ IDEA;
2022-03-05, by wenzelm
tuned;
2022-03-05, by wenzelm
clarified command-line options;
2022-03-05, by wenzelm
update official Isabelle release, notably for "Admin/init -R";
2022-03-05, by wenzelm
more robust;
2022-03-04, by wenzelm
build component for VSCodium (cross-compiled from sources for all platforms);
2022-03-04, by wenzelm
tuned signature: more robust operation;
2022-03-04, by wenzelm
clarified order;
2022-03-04, by wenzelm
proper antiquotations (amending ff784d5a5bfb);
2022-03-04, by wenzelm
clarified signature: file operations take standard_path as in Isabelle/ML/Scala;
2022-03-03, by wenzelm
provide symbols statically via ISABELLE_VSCODE_WORKSPACE, instead of LSP/PIDE protocol;
2022-03-03, by wenzelm
proper init of non-existing file;
2022-03-03, by wenzelm
proper function call;
2022-03-03, by wenzelm
clarified signature;
2022-03-03, by wenzelm
tuned;
2022-03-03, by wenzelm
tuned, based on suggestions by IntelliJ IDEA;
2022-03-03, by wenzelm
tuned;
2022-03-03, by wenzelm
clarified signature;
2022-03-03, by wenzelm
clarified modules: more uniform .scala vs. ts (amending 4519eeefe3b5);
2022-03-03, by wenzelm
misc tuning, based on suggestions by IntelliJ IDEA;
2022-03-03, by wenzelm
clarified signature;
2022-03-03, by wenzelm
tuned signature;
2022-03-03, by wenzelm
clarified signature;
2022-03-03, by wenzelm
tuned imports;
2022-03-03, by wenzelm
clarified signature;
2022-03-03, by wenzelm
clarified signature;
2022-03-03, by wenzelm
tuned signature;
2022-03-03, by wenzelm
misc tuning, based on suggestions by IntelliJ IDEA;
2022-03-03, by wenzelm
clarified modules;
2022-03-02, by wenzelm
support for file-system operations;
2022-03-02, by wenzelm
tuned signature;
2022-03-02, by wenzelm
follow standard Isabelle license --- no longer published on market place;
2022-03-02, by wenzelm
tuned README;
2022-03-02, by wenzelm
disregard public marketplace;
2022-03-02, by wenzelm
tuned imports;
2022-03-02, by wenzelm
more robust;
2022-03-02, by wenzelm
merged
2022-03-02, by wenzelm
tuned message;
2022-03-02, by wenzelm
clarified module;
2022-03-02, by wenzelm
tuned comments;
2022-03-02, by wenzelm
added documentation for new VSCode modules;
2022-03-02, by Fabian Huch
proper monospace font for terminal;
2022-03-02, by wenzelm
merged
2022-03-02, by wenzelm
tuned;
2022-03-02, by wenzelm
support system path representations (as in Isabelle/Java/Scala);
2022-03-02, by wenzelm
auto-update;
2022-03-02, by wenzelm
more robust;
2022-03-02, by wenzelm
clarified modules;
2022-02-28, by wenzelm
clarified rendering;
2022-02-28, by wenzelm
prefer hardwired locale;
2022-02-28, by wenzelm
more aggressive activation;
2022-02-28, by wenzelm
Added some theorems (from Wetzel)
2022-03-01, by paulson
tuned;
2022-02-28, by wenzelm
tuned;
2022-02-28, by wenzelm
tuned message;
2022-02-28, by wenzelm
disable extension updates;
2022-02-28, by wenzelm
tuned message;
2022-02-28, by wenzelm
disable check for updates: support just one static version;
2022-02-28, by wenzelm
misc tuning based on comments by Heiko Eißfeldt;
2022-02-27, by wenzelm
misc tuning based on comments by Heiko Eißfeldt;
2022-02-27, by wenzelm
removed junk;
2022-02-26, by wenzelm
some updates to README.md;
2022-02-26, by wenzelm
clarified default settings;
2022-02-26, by wenzelm
tuned whitespace;
2022-02-26, by wenzelm
support Isabelle fonts via patch of vscode resources;
2022-02-26, by wenzelm
proper Presentation.Entity_Context for hyperlinks (amending da1108a6d249);
2022-02-25, by wenzelm
clarified symbolic path;
2022-02-25, by wenzelm
clarified extension name (again);
2022-02-25, by wenzelm
removed obsolete material;
2022-02-25, by wenzelm
update scripts, based on recent "yo code" template;
2022-02-25, by wenzelm
clarified extension name (again), corresponding to qualified resources within VSCode (settings, commands, etc.);
2022-02-25, by wenzelm
clarified signature;
2022-02-25, by wenzelm
clarified extension name;
2022-02-25, by wenzelm
clarified signature;
2022-02-25, by wenzelm
clarified signature;
2022-02-25, by wenzelm
clarified options;
2022-02-25, by wenzelm
support local .vsix installation;
2022-02-25, by wenzelm
formal record of generated package-lock.json;
2022-02-25, by wenzelm
pro-forma update of version, for ongoing development;
2022-02-25, by wenzelm
updated notes on Isabelle/VSCode development;
2022-02-25, by wenzelm
proper engines.vscode (amending c04ccea8bdd2): required for "vsce package", e.g. via "isabelle build_vscode;
2022-02-25, by wenzelm
simp rules for negative numerals
2022-02-24, by haftmann
updated vscode extension: proper recoding;
2022-02-23, by Fabian Huch
tuned vscode extension;
2022-02-23, by Fabian Huch
tuned vscode extension: split isabelle fsp into workspace and mapping;
2022-02-23, by Fabian Huch
update VSCode plugin dependencies;
2022-02-23, by Fabian Huch
added Isabelle output panel to VSCode extension;
2022-02-23, by Fabian Huch
Simplified a couple of extremely long and ugly apply-proofs
2022-02-23, by paulson
merged
2022-02-22, by wenzelm
some updates to README.md;
2022-02-22, by wenzelm
refer to Isabelle settings via environment, which is provided via "isabelle vscode";
2022-02-22, by wenzelm
more operations;
2022-02-22, by wenzelm
more robust startup wrt. VSCode workspace (by Fabian Huch);
2022-02-22, by wenzelm
various improvements to Isabelle/VSCode (by Denis Paluca and Fabian Huch);
2022-02-22, by wenzelm
have Sledgehammer honor 'smt_nat_as_int' option
2022-02-22, by blanchet
more handling of Zipperposition definitions in Isar proof construction
2022-02-22, by blanchet
handle Zipperposition definitions in Isar proof construction
2022-02-22, by blanchet
parse Zipperposition definitions
2022-02-22, by blanchet
clarified URL;
2022-02-21, by wenzelm
clarified pdf path;
2022-02-21, by wenzelm
HTTP view of Isabelle PDF documentation;
2022-02-21, by wenzelm
clarified signature;
2022-02-21, by wenzelm
more robust;
2022-02-21, by wenzelm
tuned message;
2022-02-21, by wenzelm
clarified signature: more explicit section structure;
2022-02-21, by wenzelm
clarified signature;
2022-02-21, by wenzelm
clarified signature;
2022-02-21, by wenzelm
tuned signature;
2022-02-21, by wenzelm
tuned;
2022-02-21, by wenzelm
clarified URL (again);
2022-02-21, by wenzelm
more robust toplevel url: allow extra "/";
2022-02-21, by wenzelm
clarified signature;
2022-02-21, by wenzelm
clarified signature;
2022-02-20, by wenzelm
clarified signature;
2022-02-20, by wenzelm
support for PDF.js: platform-independent PDF viewer;
2022-02-20, by wenzelm
more robust mime_type;
2022-02-20, by wenzelm
merged
2022-02-18, 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;
2022-02-18, by wenzelm
one new lemma
2022-02-18, by paulson
clarified options;
2022-02-18, by wenzelm
clarified options;
2022-02-18, by wenzelm
clarified directory;
2022-02-18, by wenzelm
tuned whitespace;
2022-02-18, by wenzelm
prefer strict equality, without implicit type conversion;
2022-02-18, by wenzelm
tuned;
2022-02-18, by wenzelm
auto-update by VSCode;
2022-02-18, by wenzelm
more activationEvents, as proposed by Denis Paluca;
2022-02-18, by wenzelm
tuned message;
2022-02-18, by wenzelm
NEWS;
2022-02-18, by wenzelm
run Isabelle/VSCode using local VSCodium installation;
2022-02-18, by wenzelm
provide macos_exe, based on bin/codium from linux;
2022-02-18, by wenzelm
clarified options;
2022-02-18, by wenzelm
Avoid overaggresive splitting.
2022-02-17, by haftmann
more lemmas for distribution
2022-02-17, by haftmann
Avoid overaggresive simplification.
2022-02-17, by haftmann
merged
2022-02-17, by wenzelm
setup VSCode from VSCodium distribution;
2022-02-17, by wenzelm
more robust package_dir, to increase chances that it works with IntelliJ IDEA;
2022-02-17, by wenzelm
NEWS
2022-02-16, by desharna
Mirabelle now considers goals preceding "unfolding" and "using" commands
2022-02-16, by desharna
merged
2022-02-15, by paulson
an assortment of new or stronger lemmas
2022-02-15, by paulson
obsolete (reverting b3d6bb2ebf77): Isabelle/Naproche cache is now value-oriented;
2022-02-15, by wenzelm
print outcome of Sledgehammer search in panel
2022-02-14, by blanchet
print Sledgehammer error message
2022-02-14, by blanchet
updated documentation to current matter of affairs
2022-02-12, by haftmann
unused;
2022-02-10, by wenzelm
clarified signature;
2022-02-10, by wenzelm
merged
2022-02-10, by desharna
added Isabelle identification to Mirabelle output
2022-02-09, by desharna
uniformized fact selection for ATP and SMT in Sledgehammer
2022-02-09, by desharna
provide cache for slow computations;
2022-02-09, by wenzelm
used max_facts and fact_filter from slice for both ATP and SMT in sledgehammer
2022-02-09, by desharna
more operations;
2022-02-09, by wenzelm
more liberal parsing of Sledgehammer options to allow empty lists (as suggested by Larry Paulson)
2022-02-09, by blanchet
more robust TSTP proof parsing
2022-02-07, by blanchet
added possibility of extra options to SMT slices
2022-02-07, by blanchet
tuned output syntax: Hoare triples are now blocks
2022-02-04, by nipkow
tuned output syntax: INV and VAR are now blocks
2022-02-03, by nipkow
more precise slicing computation and output when not enough lemmas are available (e.g. with the 'only' syntax 'sledgehammer (lem1 lem2 lem3)')
2022-02-02, by blanchet
enable induction in one of Zipperposition's slices
2022-02-02, by blanchet
made sorting of Vampire facts more robust in the face of names that deviate from the standard scheme
2022-02-01, by blanchet
robustly handle empty proof blocks in Isar proof output
2022-02-01, by blanchet
propagate right result when enough proofs have been found
2022-02-01, by blanchet
correctly parse E proofs that assume '=' and '!=' bind more tightly than connectives
2022-02-01, by blanchet
don't lose error messages
2022-02-01, by blanchet
don't pass --auto-schedule to E indiscriminately -- use it instead of 'auto' in one slice
2022-02-01, by blanchet
careful with partial applications
2022-02-01, by blanchet
don't perform preplaying steps if preplaying is disabled
2022-02-01, by blanchet
adjust TPTP THF parser to give priority to @ over other operators, to parse Ehoh proofs
2022-02-01, by blanchet
tuned punctuation
2022-02-01, by blanchet
handle TPTP '!=' more gracefully in Isar proof reconstruction
2022-02-01, by blanchet
guard against duplicate lines in Zipperposition proofs
2022-02-01, by blanchet
tuning
2022-02-01, by blanchet
tuned NEWS
2022-02-01, by blanchet
compile HOL-TPTP
2022-01-31, by blanchet
compile Metis_Examples
2022-01-31, by blanchet
more NEWS
2022-01-31, by blanchet
compile mirabelle
2022-01-31, by blanchet
tweaked Auto Sledgehammer's behavior and output
2022-01-31, by blanchet
updated NEWS
2022-01-31, by blanchet
removed experimental prover z3_tptp
2022-01-31, by blanchet
print more verbose information
2022-01-31, by blanchet
run all installed provers by default
2022-01-31, by blanchet
update slice options centrally
2022-01-31, by blanchet
further work on new Sledgehammer slicing
2022-01-31, by blanchet
tweaked verbose output
2022-01-31, by blanchet
tweak padding of prover slice schedule to include all provers
2022-01-31, by blanchet
implemented 'max_proofs' mechanism
2022-01-31, by blanchet
document new option 'max_proofs'
2022-01-31, by blanchet
crude implementation of centralized slicing
2022-01-31, by blanchet
removed obscure E option
2022-01-31, by blanchet
take 'induction_rules' into consideration, as well as 'max_facts' even when 'only' is set
2022-01-31, by blanchet
rationalize slicing format
2022-01-31, by blanchet
thread slices through
2022-01-31, by blanchet
simplified 'best_slice' data structure and made minor changes to slices
2022-01-31, by blanchet
changed logic of 'slice' option to 'slices'
2022-01-31, by blanchet
updated documentation of 'slice' (now 'slices') option
2022-01-31, by blanchet
revised Sledgehammer documentation
2022-01-31, by blanchet
rationalized output for forthcoming slicing model
2022-01-31, by blanchet
use same default for FO and HO provers w.r.t. induction principles, based on evaluation -- this also simplifies the code
2022-01-31, by blanchet
disable slicing within ATP module (in preparation for refactoring)
2022-01-31, by blanchet
disable slicing within SMT (in preparation for factoring it out)
2022-01-31, by blanchet
generalized the 'slice' option towards more flexible slicing
2022-01-31, by blanchet
tuned -- fewer warnings;
2022-01-31, by wenzelm
Added a tiny proof
2022-01-29, by paulson
Deletion of a duplicate proof
2022-01-28, by paulson
useful lemma integral_less
2022-01-27, by paulson
merged
2022-01-27, by desharna
removed unused parameter following f9908452b282
2022-01-26, by desharna
treat 'using X by meson' as 'by (meson X)' to avoid loss of polymorphism (cf. metis)
2022-01-26, by blanchet
fixed dodgy intro! attributes
2022-01-25, by paulson
merged
2022-01-25, by desharna
optimized facts traversal in TPTP translation
2022-01-22, by desharna
optimized app_op_level selection in TPTP generation
2022-01-22, by desharna
tuned trivial check in mirabelle_sledgehammer
2022-01-22, by desharna
renamed run_action to run in Mirabelle.action record
2022-01-22, by desharna
added spying of fact filtering timing
2022-01-22, by desharna
tuned mirabelle_sledgehammer output
2022-01-22, by desharna
added spying to Sledgehammer
2022-01-21, by desharna
proper fact filter for dummy ATPs
2022-01-21, by desharna
added syping of fact filtering time to sledgehammer
2022-01-21, by desharna
removed unsynchronized references in mirabelle_sledgehammer
2022-01-21, by desharna
tuned mirabelle_sledgehammer to have a single call to Synchronized.change per run
2022-01-21, by desharna
updated to polyml-test-15c840d48c9a;
build_history_base_arm
2022-01-24, by wenzelm
some updates and clarification on Assumption.export_term;
2022-01-22, by wenzelm
new theorem has_integral_UN
2022-01-21, by paulson
updated to jdk-17.0.2+8;
2022-01-21, by wenzelm
used elapsed time instead of cpu time in Mirabelle because the latter contain cpu time of all threads
2022-01-21, by desharna
NEWS
2022-01-20, by desharna
added Mirabelle option "-y" for dry run
2022-01-20, by desharna
tuned garbage optimization
2022-01-20, by desharna
added cpu time (in ms) to Mirabelle run_action output
2022-01-19, by desharna
added Mirabelle option -r to randomize the goals before selection
2022-01-18, by desharna
A new lemma about inverse image
2022-01-17, by paulson
proper treatment of $let variables in symbol table in Sledgehammer
2022-01-16, by desharna
removed unconditional TPTP symbol declaration for undefined_bool in sledgehammer
2022-01-15, by desharna
merged
2022-01-12, by desharna
split option "sledgehammer_atp_dest_dir" into "sledgehammer_atp_prob_dest_dir" and "sledgehammer_atp_proof_dest_dir"
2022-01-11, by desharna
proper name mangling of "undefined" constants in Sledgehammer
2022-01-11, by desharna
earlier availability of lifting
2022-01-11, by haftmann
more correct transfer
2022-01-11, by haftmann
merged
2022-01-10, by desharna
proper abstraction of function variables when instantiating induction rules in Sledgehammer
2022-01-10, by desharna
added lemma asympD
2022-01-10, by desharna
added lemma
2022-01-10, by nipkow
Some lemmas about continuous functions with integral zero
2022-01-09, by paulson
merged
2022-01-07, by desharna
added lemmas wf_imp_asym, wfP_imp_asymp, and wfP_imp_irreflp
2022-01-06, by desharna
removed $ite from E 2.6 in THF format
2022-01-05, by desharna
New and simplified theorems
2022-01-05, by paulson
merged
2022-01-03, by desharna
prefixed all mirabelle_sledgehammer output lines with sledgehammer output
2022-01-03, by desharna
added lemma
2021-12-29, by nipkow
Tiny additions inspired by Roth development
2021-12-26, by paulson
allow general command transactions with presentation;
2021-12-21, by wenzelm
more operations;
2021-12-21, by wenzelm
clarified signature;
2021-12-21, by wenzelm
tuned signature;
2021-12-21, by wenzelm
support Gradle as alternative to Maven (again);
2021-12-21, by wenzelm
tuned mirabelle command-line help message
2021-12-20, by desharna
updated Mirabelle documentation
2021-12-20, by desharna
proper documentation for induction_rules Sledgehammer option
2021-12-20, by desharna
NEWS
2021-12-19, by desharna
merged
2021-12-19, by desharna
used TH1 for Leo-III in sledgehammer
2021-12-18, by desharna
tuned run_sledgehammer and called it directly from Mirabelle
2021-12-18, by desharna
exported Sledgehammer.launch_prover and use it in Mirabelle
2021-12-18, by desharna
proper filtering inf induction rules in Mirabelle
2021-12-18, by desharna
added nearly_all_facts_of_context and uniformized its usage in Sledgehammer and Mirabelle
2021-12-17, by desharna
tuned ATP to use is_widely_irrelevant_const
2021-12-17, by desharna
added support for initialization messages to Mirabelle
2021-12-17, by desharna
tuned comment
2021-12-17, by blanchet
support for JSON:API;
2021-12-15, by wenzelm
support for Flarum server;
2021-12-15, by wenzelm
tuned whitespace;
2021-12-15, by wenzelm
tuned imports;
2021-12-15, by wenzelm
tuned comments;
2021-12-15, by wenzelm
clarified author names;
2021-12-15, by wenzelm
clarified author names;
2021-12-15, by wenzelm
merged
2021-12-14, by wenzelm
more accurate names;
2021-12-14, by wenzelm
more standard author_info;
2021-12-14, by wenzelm
clarified author info and cluster nodes;
2021-12-14, by wenzelm
more data integrity: name vs. address;
2021-12-14, by wenzelm
clarified signature: more operations;
2021-12-14, by wenzelm
clarified signature;
2021-12-14, by wenzelm
tuned;
2021-12-14, by wenzelm
more data integrity: name vs. address;
2021-12-14, by wenzelm
tuned comments;
2021-12-14, by wenzelm
merged
2021-12-14, by desharna
tuned ATP to use fold_index
2021-12-13, by desharna
tuned sledgehammer to use map_index
2021-12-10, by desharna
merged
2021-12-13, by wenzelm
more data integrity: name vs. address;
2021-12-13, by wenzelm
misc tuning and clarification;
2021-12-13, by wenzelm
clarified name;
2021-12-13, by wenzelm
more mailing list content;
2021-12-13, by wenzelm
more mailing list content;
2021-12-13, by wenzelm
updated links;
2021-12-13, 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;
2021-12-11, by wenzelm
tuned ATP to use map_index
2021-12-10, by desharna
removed obsolete RC tags;
2021-12-12, by wenzelm
proper path;
2021-12-12, by wenzelm
merged, resolving conflict in src/Doc/Implementation/Logic.thy;
2021-12-12, by wenzelm
Added tag Isabelle2021-1 for changeset c2a2be496f35
2021-12-12, by wenzelm
tuned;
Isabelle2021-1
2021-12-11, by wenzelm
proper ML types (amending 1aa92bc4d356);
2021-12-07, by wenzelm
proper types for Scala.Fun instances (amending 1aa92bc4d356);
2021-12-07, by wenzelm
proper syntax category;
2021-12-07, by wenzelm
provide component naproche-20211211;
2021-12-11, by wenzelm
merged
2021-12-10, by wenzelm
more Mailman archives;
2021-12-10, by wenzelm
more Mailman content;
2021-12-10, by wenzelm
clarified signature;
2021-12-10, by wenzelm
tuned metis to use map_index
2021-12-10, by desharna
merged
2021-12-10, by desharna
fixed HOL-TPTP
2021-12-10, by desharna
tuned vars_of_iterm
2021-12-09, by desharna
fixed TPTP generation of multi-arity expressions
2021-12-07, by desharna
proper handling of Hilbert choice in TFX logics
2021-11-29, by desharna
proper tptp_builtins
2021-11-28, by desharna
reused Sledgehammer code to parse parameters of sledgehammer action in Mirabelle
2021-11-28, by desharna
proper proxy for Hilbert choice in TPTP output
2021-11-21, by desharna
proper polymorphism for TH1 format in Sledgehammer
2021-11-19, by desharna
refactored $ite and $let configuration and added dummy_thf_reduced prover
2021-11-19, by desharna
tuned TPTP file names generated by Sledgehammer
2021-11-17, by desharna
tuned SMT-Lib file names generated by Mirabelle
2021-11-17, by desharna
added support for higher-order SMT proof search in Sledgehammer
2021-11-17, by desharna
separated FOOL from $ite/$let in TPTP output
2021-11-12, by desharna
missing latex font
2021-12-09, by nipkow
Rewrite: added links to docu, made more prominent
2021-12-09, by nipkow
discontinued old-style {* verbatim *} tokens;
2021-12-06, by wenzelm
tuned proof;
2021-12-06, by wenzelm
isabelle update_cartouches;
2021-12-06, by wenzelm
more symbolic latex_output via XML (using YXML within text);
2021-12-05, by wenzelm
tuned signature: remove unused;
2021-12-05, by wenzelm
prefer symbolic Latex.environment (typeset in Isabelle/Scala);
2021-12-05, by wenzelm
tuned signature;
2021-12-05, by wenzelm
clarified corner cases of syntax;
2021-12-05, by wenzelm
clarified Parse.embedded_ml: follow documentation (8baf2e8b16e2);
2021-12-05, by wenzelm
a slightly simpler proof
2021-12-04, by paulson
provide component naproche-2d99afe5c349;
2021-12-04, by wenzelm
merged
2021-12-04, by wenzelm
Added tag Isabelle2021-1-RC5 for changeset 8baf2e8b16e2
2021-12-04, by wenzelm
more documentation about Type/Const antiquotations;
2021-12-03, by wenzelm
more documentation about document build options;
2021-12-03, by wenzelm
address problems with launch4j and jdk-17 (see also 41d009462d3c, copy of 41d009462d3c);
2021-12-03, by wenzelm
tuned --- fewer IDE warnings;
2021-12-02, by wenzelm
more robust physical timeout (despite 1bea05713dde), especially relevant for quickcheck where large unary numerals may cause excessive heap allocations and resulting GC is better included in the timing;
2021-11-30, by wenzelm
added definitions multp{DM,HO} and corresponding lemmas
2021-11-28, by desharna
added wfP_less to wellorder and wfP_less_multiset
2021-11-28, by desharna
restored lemmas less_multiset{DM,HO} inadvertently changed by c256bba593f3
2021-11-28, by desharna
merged
2021-11-27, by desharna
added lemmas irreflp_{less,greater} to preorder and {trans,irrefl}_mult{,p} to Multiset
2021-11-27, by desharna
redefined less_multiset to be based on multp
2021-11-27, by desharna
added lemmas multp_code_eq_multp and multeqp_code_eq_reflclp_multp
2021-11-27, by desharna
added lemmas multp_cancel, multp_cancel_add_mset, and multp_cancel_max
2021-11-27, by desharna
added lemmas multp_implies_one_step, one_step_implies_multp, and subset_implies_multp
2021-11-27, by desharna
added lemma wfP_multp
2021-11-27, by desharna
added lemma mono_multp
2021-11-27, by desharna
added Multiset.multp as predicate equivalent of Multiset.mult
2021-11-26, by desharna
address problems with launch4j and jdk-17 (see also 41d009462d3c);
2021-11-27, by wenzelm
more robust build on midrange hardware;
2021-11-27, by wenzelm
clarified tests: omit somewhat pointless (unstable) results;
2021-11-27, by wenzelm
proper fields for gnuplot (amending b614e3e4146a);
2021-11-27, by wenzelm
tuned output;
2021-11-27, by wenzelm
tuned;
2021-11-27, by wenzelm
merged
2021-11-26, by wenzelm
more robust build on midrange hardware (despite 67d6f1708ea4);
2021-11-26, by wenzelm
Added tag Isabelle2021-1-RC4 for changeset 2336356d4180
2021-11-26, by wenzelm
updated to polyml-5.9;
2021-11-26, by wenzelm
NEWS on "isabelle mirabelle";
2021-11-26, by wenzelm
tuned;
2021-11-26, by wenzelm
clarified default for kodkod_scala;
2021-11-25, by wenzelm
maintain option kodkod_scala within theory context, to allow local modification;
2021-11-25, by wenzelm
NEWS for proper release;
2021-11-25, by wenzelm
updated to flatlaf-1.6.4;
2021-11-25, by wenzelm
avoid broken links: auxiliary files are not yet supported;
2021-11-25, by wenzelm
option document_comment_latex supports e.g. Dagstuhl LIPIcs;
2021-11-24, by wenzelm
more explicit type Latex.Tags;
2021-11-24, by wenzelm
more uniform treatment of optional_argument for Latex elements;
2021-11-24, by wenzelm
removed pointless 'text_cartouche' command: regular 'text' already supports cartouches;
2021-11-23, by wenzelm
example: alternative document headings, based on more general document output markup;
2021-11-23, by wenzelm
more general document output: enclosing markup is defined in user-space;
2021-11-23, by wenzelm
clarified modules (see c299abcf7081);
2021-11-23, by wenzelm
output for document commands like 'section', 'text' is defined in user-space, as part of the command transaction;
2021-11-23, by wenzelm
clarified modules;
2021-11-23, by wenzelm
tuned signature: more explicit types for presentation;
2021-11-23, by wenzelm
more robust support for Windows line-endings;
2021-11-22, by wenzelm
source positions for document markup commands, e.g. to retrieve PIDE markup in presentation;
2021-11-22, by wenzelm
more compact data during presentation: Entity_Context.Theory_Export instead of full Export_Theory.Theory;
2021-11-22, by wenzelm
clarified system option standard values: avoid oddities like "isabelle build -o document_output" producing directories named "true";
2021-11-21, by wenzelm
more symbolic latex_output via XML (using YXML within text);
2021-11-20, by wenzelm
proper enclose_name (amending e77c5bfca9aa);
2021-11-20, by wenzelm
Latex.Output.latex_heading depends on option document_heading_prefix, e.g. relevant for Dagstuhl LIPIcs which prefers unaliased \section etc.;
2021-11-20, by wenzelm
more symbolic latex_output via XML;
2021-11-20, by wenzelm
clarified hook for Mirabelle (again): cover all 'theories' sections within ROOT (see also 9ead8d9be3ab);
2021-11-20, by wenzelm
tuned;
2021-11-20, by wenzelm
tuned;
2021-11-20, by wenzelm
updated to verit-2021.06.2-rmx;
2021-11-19, by wenzelm
clarified HTML_Context.theory_exports: prefer value-oriented parallelism;
2021-11-17, by wenzelm
generate problems with correct logic for veriT
2021-11-17, by fleury
more parallelism, at the cost of potential duplicates of make_thy;
2021-11-17, by wenzelm
afford more parallelism for sessions (instead of theories in 5eac4b13d1f1): depend on disjoint data areas (notably base.session_theories in 2ad892ac749a);
2021-11-17, by wenzelm
more interrupts;
2021-11-17, by wenzelm
present only selected session theories (as in Isabelle2021), in contrast to 2bc24136bdeb, eb89b3a37826;
2021-11-17, by wenzelm
tuned;
2021-11-17, by wenzelm
clarified modules;
2021-11-17, by wenzelm
tuned (see also e0d1d9203275);
2021-11-17, by wenzelm
clarified signature;
2021-11-17, by wenzelm
tuned;
2021-11-17, by wenzelm
spelling;
2021-11-16, by wenzelm
added asymp_{less,greater} to preorder and moved mult1_lessE out
2021-11-25, by desharna
renamed multp_code_iff and multeqp_code_iff
2021-11-25, by desharna
simplified mult_cancel_max and introduced orginal lemma as mult_cancel_max0
2021-11-25, by desharna
renamed Multiset.multp and Multiset.multeqp
2021-11-25, by desharna
added lemmas
2021-11-17, by nipkow
merged
2021-11-16, by wenzelm
tuned;
2021-11-16, by wenzelm
removed redundant test (see also 86fac52c2795, a9fea3f11cc0);
2021-11-16, by wenzelm
just one Presentation.State for all sessions: avoid duplication of already presented theories (very slow) and cached theory export (not very slow);
2021-11-16, by wenzelm
proper version;
2021-11-16, by wenzelm
back to Z3 4.4.0pre for all platforms except arm64-linux: avoid failure e.g. in Padic_Ints (AFP/7a2522dce834);
2021-11-16, by wenzelm
less ambitious parallelism: more direct read/write saves overall heap space and GC time;
2021-11-16, by wenzelm
slightly faster XML output: avoid too much regrowing of StringBuilder;
2021-11-16, by wenzelm
updated NEWS: arm64-linux support is almost complete;
2021-11-15, by wenzelm
update z3-4.4.0pre-3 to z3-4.4.1, which happens to have an arm64_linux executable in Debian 9;
2021-11-15, by wenzelm
more material for HOL-Analysis.Infinite_Sum
2021-11-15, by Manuel Eberl
more symbolic latex_output via XML;
2021-11-15, by wenzelm
clarified signature;
2021-11-15, by wenzelm
updated to polyml-5.9-610a153b941d -- close to final;
2021-11-14, by wenzelm
tuned signature (again): latex_output is likely to depend on context;
2021-11-14, by wenzelm
more symbolic latex output;
2021-11-14, by wenzelm
tuned signature;
2021-11-14, by wenzelm
symbolic latex_output via XML, interpreted in Isabelle/Scala;
2021-11-14, by wenzelm
tuned signature;
2021-11-14, by wenzelm
clarified signature;
2021-11-14, by wenzelm
clarified signature;
2021-11-13, by wenzelm
clarified signature: more privacy;
2021-11-13, by wenzelm
tuned output --- less redundancy;
2021-11-13, by wenzelm
tuned whitespace;
2021-11-13, by wenzelm
clarified signature: Latex.Output as parameter to Document_Build.Engine;
2021-11-13, by wenzelm
proper detection of ARM platform variants;
2021-11-12, by wenzelm
back to post-release mode;
2021-11-12, by wenzelm
updated for release;
2021-11-12, by wenzelm
Added tag Isabelle2021-1-RC3 for changeset 2b212c8138a5
2021-11-12, by wenzelm
merged
2021-11-12, by wenzelm
updated to polyml-5.9-cc80e2b43c38, which also contains ARM64 on darwin (unused by default);
2021-11-12, by wenzelm
clarified HTML_Context: more explicit directory structure;
2021-11-12, by wenzelm
tuned comments;
2021-11-12, by wenzelm
tuned;
2021-11-12, by wenzelm
clarified signature;
2021-11-12, by wenzelm
clarified properties: avoid empty entry;
2021-11-12, by wenzelm
tuned signature;
2021-11-12, by wenzelm
merged
2021-11-12, by nipkow
tuned (thanks to J. Villadsen)
2021-11-12, by nipkow
added padding to Mirabelle's output
2021-11-12, by desharna
merged
2021-11-12, by desharna
tuned generation of TPTP with $ite/$let in higher-order logics
2021-11-11, by desharna
tuned generation of TPTP with $ite in function position
2021-11-11, by desharna
tuned TPTP generation of If helper facts
2021-11-11, by desharna
merged
2021-11-11, by wenzelm
clarified signature: prefer static operations;
2021-11-11, by wenzelm
clarified signature: avoid potential misunderstanding of Resources.empty as proper Resources;
2021-11-11, by wenzelm
more robust;
2021-11-11, by wenzelm
tuned signature;
2021-11-11, by wenzelm
clarified signature: more explicit class Entity_Context with private state + operations;
2021-11-11, by wenzelm
more hyperlinks, notably internal fact references;
2021-11-11, by wenzelm
Automated merge with bundle:/var/folders/9z/l1x9y3bd16x9_70pdp4703jr0000gp/T/SourceTreeTemp.14UUXO
2021-11-11, by paulson
A tiny bit of tidying connected with Zorn's Lemma
2021-11-09, by paulson
tuned;
2021-11-10, by wenzelm
tuned;
2021-11-10, by wenzelm
proper handling of Protocol.Export, using the payload from the message --- in contrast db_context.read_export materializes only later by a different thread (race condition);
2021-11-10, by wenzelm
revert temporary workaround 6d111935299c;
2021-11-10, by wenzelm
added lemma
2021-11-10, by nipkow
merged
2021-11-09, by nipkow
tuned attributes to avoid looping
2021-11-09, by nipkow
added eq_iff_swap for creating symmetric variants of thms; applied it in List.
2021-11-08, by nipkow
tuned text;
2021-11-09, by wenzelm
more robust timeout, following df4449c6eff1;
2021-11-09, by wenzelm
more accurate Files.isRegularFile, exclude directories (e.g. jar_path);
2021-11-09, by wenzelm
proper java_version for isabelle_setup;
2021-11-09, by wenzelm
explicit option metric_argo_timeout, with reasonable default for Raspberry Pi;
2021-11-08, by wenzelm
tuned;
2021-11-08, by wenzelm
repackage minisat-2.2.1 with cygwin1.dll: required to run the executable without existing Cygwin context (normally provided by bash_process);
2021-11-08, by wenzelm
discontinued redundant document_preprocessor: in the worst case, a plain-old document/build script will do;
2021-11-08, by wenzelm
clarified messages, depending on option "document_echo";
2021-11-08, by wenzelm
just one cache, via HTML_Context, via Sessions.Store or Session;
2021-11-08, by wenzelm
merged
2021-11-08, by paulson
new lemmas about convex, concave functions, + tidying
2021-11-07, by paulson
proper support for arm64;
2021-11-07, by wenzelm
no perl (amending 59ef23ac81ab);
2021-11-07, by wenzelm
merged
2021-11-07, by wenzelm
Added tag Isabelle2021-1-RC2 for changeset b92b5a57521b
2021-11-07, by wenzelm
merged
2021-11-07, by nipkow
Preserve variable name z in VAR {z = t}
2021-11-07, by nipkow
back to scala-2.13.5: avoid crash of Scala REPL on arm64-darwin;
2021-11-07, by wenzelm
updated to polyml-5.9-5d4caa8f7148, which also contains ARM64 on darwin (unused by default);
2021-11-07, by wenzelm
more precise URL
2021-11-07, by nipkow
tuned page breaks
2021-11-07, by nipkow
cover all possible kinds, notably for references outside of this theory (amending 129fb11b357f);
2021-11-06, by wenzelm
proper foundational order;
2021-11-06, by wenzelm
back to non-strict Export_Theory.read_theory (without warning): theories could have been skipped due to "condition";
2021-11-06, by wenzelm
use all entity kinds from theory export, e.g. "method", "attribute";
2021-11-06, by wenzelm
clarified signature;
2021-11-06, by wenzelm
clarified physical_ref;
2021-11-06, by wenzelm
proper treatment of session build hierarchy;
2021-11-06, by wenzelm
proper used_theories for session build hierarchy, not known_theories from imported sessions;
2021-11-06, by wenzelm
present theories from imported sessions as required;
2021-11-05, by wenzelm
avoid multiple copies of fonts;
2021-11-05, by wenzelm
more compact persistent data;
2021-11-05, by wenzelm
tuned;
2021-11-05, by wenzelm
proper term_cache;
2021-11-05, by wenzelm
prefer "NAME|KIND" format, as already used in Isabelle/MMT and Isabelle/Dedukti;
2021-11-05, by wenzelm
tuned;
2021-11-05, by wenzelm
observer proper session hierarchy (according to build_graph): thus exported artifacts are always valid;
2021-11-05, by wenzelm
tuned;
2021-11-05, by wenzelm
clarified order: prefer bottom-up construction of partial content;
2021-11-05, by wenzelm
more thorough update_global_index: overwrite old content;
2021-11-05, by wenzelm
tuned;
2021-11-05, by wenzelm
tuned;
2021-11-05, by wenzelm
clarified HTML_Context: just one context type;
2021-11-05, by wenzelm
unused (see also 217e6cf61453, 5e7916535860);
2021-11-05, by wenzelm
merged
2021-11-04, by wenzelm
clarified Theory_Cache: prefer immutable data with Synchronized variable;
2021-11-04, by wenzelm
tuned signature;
2021-11-04, by wenzelm
unused;
2021-11-04, by wenzelm
proper support of verit's return code for timeout
2021-11-04, by Mathias Fleury
tuned whitespace;
2021-11-04, by wenzelm
updated to verit-2021.06.1-rmx, to address "Abnormal termination with exit code 14";
2021-11-04, by wenzelm
clarified signature;
2021-11-04, by wenzelm
prefer official Export.explode_name;
2021-11-04, by wenzelm
tuned;
2021-11-04, by wenzelm
avoid conflict with future keyword;
2021-11-04, by wenzelm
tuned messages;
2021-11-04, by wenzelm
clarified signature: more direct XML.symbol_length;
2021-11-04, by wenzelm
more direct Symbol.length: Symbol.decode is redundant, symbol counts are invariant under it;
2021-11-04, by wenzelm
tuned -- eliminate clones stemming from d28a51dd9da6;
2021-11-04, by wenzelm
more to ANNOUNCE;
2021-11-03, by wenzelm
clarified link style: similar to Isabelle/jEdit;
2021-11-03, by wenzelm
tuned;
2021-11-03, by wenzelm
improved HTML presentation by Fabian Huch;
2021-11-03, by wenzelm
proper HTTPS;
2021-11-03, by wenzelm
proper markup type (amending be49c660ebbf);
2021-11-03, by wenzelm
merged;
2021-11-03, by wenzelm
more PIDE markup;
2021-11-03, by wenzelm
tuned signature;
2021-11-03, by wenzelm
more PIDE markup;
2021-11-03, by wenzelm
recover library_index_content.template from c337c798f64c: required for website/build/main;
2021-11-03, by wenzelm
merged
2021-11-03, by paulson
simplified some ugly proofs
2021-11-02, by paulson
more generous timeout: support build on Raspberry Pi;
2021-11-03, by wenzelm
add documentation for pred_mono
2021-11-03, by traytel
merged
2021-11-03, by desharna
added "mono" attribute to BNF generated pred_mono theorems
2021-11-02, by desharna
merged
2021-11-02, by desharna
do not declare $let-bound variables in TPTP output
2021-10-29, by desharna
IDE build actually works (but somewhat pointless);
2021-11-03, by wenzelm
suppress sources from jEdit/test, which prevent regular build of the generated scala_project;
2021-11-03, by wenzelm
removed junk;
2021-11-03, by wenzelm
improve pagebreaks by *not* using supertabular too much;
2021-11-02, by wenzelm
updated to scala-2.13.7 --- problems with jline disappear after purging $HOME/.inputrc;
2021-11-02, by wenzelm
more robust "isabelle scala_project": Gradle has been replaced by Maven;
2021-11-02, by wenzelm
tuned;
2021-11-01, by wenzelm
support linux_arm as well, e.g. native Docker on Apple Silicon;
2021-11-01, by wenzelm
update paths at TUM;
2021-11-01, by wenzelm
Added tag Isabelle2021-1-RC1 for changeset 81cc8f2ea9e7
2021-11-01, by wenzelm
updated for release;
2021-11-01, by wenzelm
some reordering for release;
2021-11-01, by wenzelm
updated to jdk-17.0.1+12;
2021-11-01, by wenzelm
tuned message;
2021-11-01, by wenzelm
clarified antiquotations;
2021-10-31, by wenzelm
tuned;
2021-10-31, by wenzelm
minor performance tuning;
2021-10-31, by wenzelm
more robust;
2021-10-30, by wenzelm
provide native executables for arm64-darwin, for more robust startup without Rosetta 2;
2021-10-30, by wenzelm
tuned proofs -- avoid z3, which is unavailable on arm64-linux;
2021-10-30, by wenzelm
prefer "sat_solver = MiniSat", to make examples work uniformly on all platforms;
2021-10-30, by wenzelm
discontinued pointless check of kodkodi_version, it is implicit in the bundled component;
2021-10-30, by wenzelm
tuned proofs -- avoid z3, which is unavailable on arm64-linux;
2021-10-30, by wenzelm
tuned;
2021-10-30, by wenzelm
test version of prespective polyml-5.9;
2021-10-30, by wenzelm
clarified antiquotations;
2021-10-30, by wenzelm
updated for pre-5.9 testing;
2021-10-30, by wenzelm
clarified antiquotations;
2021-10-30, by wenzelm
clarified antiquotations;
2021-10-30, by wenzelm
clarified antiquotations;
2021-10-29, by wenzelm
more robust subgoal addressing;
2021-10-29, by wenzelm
proper subgoal addressing;
2021-10-29, by wenzelm
clarified antiquotations;
2021-10-29, by wenzelm
recursive find_eq, not find_dist;
2021-10-29, by wenzelm
misc tuning and clarification;
2021-10-29, by wenzelm
clarified antiquotations;
2021-10-29, by wenzelm
order_tac: prevent potential bug, improve perf and tracing
2021-10-29, by Lukas Stevens
misc tuning and clarification;
2021-10-29, by wenzelm
clarified antiquotations;
2021-10-29, by wenzelm
clarified antiquotations: no need for Thm.beta_conversion, due to Thm.instantiate_beta;
2021-10-29, by wenzelm
clarified antiquotations: no need for Thm.beta_conversion, due to Thm.instantiate_beta;
2021-10-29, by wenzelm
avoid persistence of static context: instantiation arguments should provide proper dynamic context (see also e2e2bc1f9570);
2021-10-29, by wenzelm
added Thm.instantiate_beta;
2021-10-29, by wenzelm
moved generic implementation into HOL-Main
2021-10-28, by haftmann
tuned;
2021-10-29, by wenzelm
tuned;
2021-10-28, by wenzelm
clarified antiquotations;
2021-10-28, by wenzelm
clarified antiquotations;
2021-10-28, by wenzelm
discontinued somewhat pointless antiquotations;
2021-10-28, by wenzelm
NEWS;
2021-10-28, by wenzelm
clarified antiquotations, assuming that Drule.instantiate_normalize was merely a historical relic;
2021-10-28, by wenzelm
clarified antiquotations;
2021-10-28, by wenzelm
clarified antiquotations;
2021-10-28, by wenzelm
clarified antiquotations;
2021-10-28, by wenzelm
clarified antiquotations;
2021-10-28, by wenzelm
support for "lemma";
2021-10-28, by wenzelm
tuned;
2021-10-28, by wenzelm
local fixes for "lemma" antiquotation;
2021-10-28, by wenzelm
clarified signature;
2021-10-28, by wenzelm
tuned;
2021-10-28, by wenzelm
clarified keywords: major take precedence for commands, but not used for antiquotations;
2021-10-28, by wenzelm
tuned modules;
2021-10-28, by wenzelm
more antiquotations;
2021-10-27, by wenzelm
moved a theorem to a sensible place
2021-10-27, by paulson
merged
2021-10-26, by wenzelm
tuned, continuing e955964d89cb;
2021-10-26, by wenzelm
avoid waste of resources due to dynamic simpset (amending 45c09620f726);
2021-10-26, by wenzelm
fix latex
2021-10-26, by Norbert Schirmer
clarified modules;
2021-10-26, by wenzelm
more generic bit/word lemmas for distribution
2021-10-26, by haftmann
merged
2021-10-26, by paulson
Added / moved some simple set-theoretic lemmas
2021-10-26, by paulson
more CONTRIBUTORS and NEWS;
2021-10-26, by wenzelm
cleanup; add Apple reference
2021-10-19, by Norbert Schirmer
refine interface
2021-07-15, by Norbert Schirmer
generalized component lookup for syntax and distinctness proofs. added some tracing.
2020-11-12, by Norbert Schirmer
merged
2021-10-25, by wenzelm
tuned;
2021-10-25, by wenzelm
more antiquotations;
2021-10-25, by wenzelm
more antiquotations;
2021-10-25, by wenzelm
more robust: genuinely free variables need to be instantiated;
2021-10-25, by wenzelm
tuned comments;
2021-10-25, by wenzelm
clarified errors;
2021-10-25, by wenzelm
tuned;
2021-10-25, by wenzelm
clarified instantiation: local beta reduction after substitution, as for Envir.expand_term_defs;
2021-10-25, by wenzelm
tuned;
2021-10-25, by wenzelm
clarified signature -- avoid clones;
2021-10-25, by wenzelm
Refinement of partitions
2021-10-25, by paulson
avoid persistence of static context: instantiation arguments should provide proper dynamic context;
2021-10-24, by wenzelm
more antiquotations;
2021-10-24, by wenzelm
more markup;
2021-10-24, by wenzelm
clarified name, syntax, messages;
2021-10-24, by wenzelm
more antiquotations;
2021-10-24, by wenzelm
more control symbols;
2021-10-24, by wenzelm
tuned signature;
2021-10-24, by wenzelm
ML antiquotations to instantiate types/terms/props;
2021-10-24, by wenzelm
tuned;
2021-10-21, by wenzelm
clarified modules;
2021-10-21, by wenzelm
clarified modules;
2021-10-20, by wenzelm
clarified modules;
2021-10-20, by wenzelm
discontinued obsolete "val extend = I" for data slots;
2021-10-20, by wenzelm
clarified modules;
2021-10-20, by wenzelm
clarified modules;
2021-10-20, by wenzelm
clarified signature;
2021-10-20, by wenzelm
tuned;
2021-10-20, by wenzelm
clarified keywords and reports;
2021-10-20, by wenzelm
clarified signature;
2021-10-20, by wenzelm
merged
2021-10-20, by desharna
proper veriT --max-time option
2021-10-19, by desharna
refactored tptp_builtins in Sledgehammer
2021-10-19, by desharna
merged
2021-10-19, by wenzelm
tuned ML --- clarified use of context;
2021-10-19, by wenzelm
tuned --- fewer clones;
2021-10-19, by wenzelm
updated to jEdit plugin Highlight 2.5;
2021-10-19, by wenzelm
proper tactic combinator;
2021-10-19, by wenzelm
proper file headers;
2021-10-19, by wenzelm
clarified context;
2021-10-19, by wenzelm
more accurate treatment of context;
2021-10-19, by wenzelm
updated email address
2021-10-19, by Manuel Eberl
removed some 'private' modifiers from HOL-Computational_Algebra
2021-10-15, by Manuel Eberl
merged
2021-10-18, by wenzelm
merged
2021-10-18, by wenzelm
more robust Variable.revert_bounds (see also b12f2cef3ee5);
2021-10-18, by wenzelm
more accurate treatment of context;
2021-10-17, by wenzelm
tuned -- proper names/scopes for contexts;
2021-10-17, by wenzelm
clarified context;
2021-10-16, by wenzelm
clarified context;
2021-10-16, by wenzelm
tuned;
2021-10-16, by wenzelm
unused;
2021-10-16, by wenzelm
more accurate treatment of context;
2021-10-16, by wenzelm
isabelle regenerate_cooper;
2021-10-15, by wenzelm
revert bbfed17243af, breaks HOL-Proofs extraction;
2021-10-15, by wenzelm
tuned;
2021-10-15, by wenzelm
tuned;
2021-10-15, by wenzelm
proper p' instead of p (amending 52c7c42e7e27);
2021-10-15, by wenzelm
proper context for Goal.prove_internal;
2021-10-15, by wenzelm
discontinued Term.dest_abs / Logic.dest_all, which are officially superseded by Variable.dest_abs etc., but there are also Term.dest_abs_global to recover existing tools easily;
2021-10-15, by wenzelm
more accurate treatment of context, notably for nested Goal.proof / SUBPROOF;
2021-10-15, by wenzelm
tuned;
2021-10-15, by wenzelm
tuned;
2021-10-15, by wenzelm
tuned;
2021-10-15, by wenzelm
spelling;
2021-10-15, by wenzelm
clarified context;
2021-10-15, by wenzelm
clarified signature;
2021-10-14, by wenzelm
tuned Vampire configuration to use TFX in Sledgehammer
2021-10-14, by desharna
added Mirabelle action presburger
2021-10-18, by desharna
added timing to Mirabelle action arith
2021-10-18, by desharna
added error message on invalid Mirabelle action
2021-10-18, by desharna
A few new lemmas plus some refinements
2021-10-15, by paulson
merged
2021-10-14, by desharna
produced Mirabelle output directly in ML until Scala output gets fixed
2021-09-20, by desharna
clarified signature;
2021-10-13, by wenzelm
clarified signature;
2021-10-13, by wenzelm
clarified signature;
2021-10-13, by wenzelm
removed unused material (left-over from fd0c85d7da38);
2021-10-13, by wenzelm
support HOL-Isar_Examples.Hoare as well (amending 403ce50e6a2a);
2021-10-13, by wenzelm
removed junk;
2021-10-13, by wenzelm
merged
2021-10-12, by nipkow
separated commands from annotations to be able to abstract about the latter only
2021-10-12, by nipkow
prefer standard Term.dest_abs, with minor deviation of generated names;
2021-10-12, by wenzelm
tuned comments;
2021-10-12, by wenzelm
more examples
2021-10-11, by nipkow
workaround for old macOS versions, after change of Let's Encrypt root certificate --- see also https://letsencrypt.org/docs/dst-root-ca-x3-expiration-september-2021 --- Java/Scala Isabelle_System.download() works, but curl doens't;
2021-10-11, by wenzelm
more complete simp rules
2021-10-11, by haftmann
more complete simp rules
2021-10-10, by haftmann
avoid overaggressive contraction of conversions
2021-10-10, by haftmann
normalizing NOT (numeral _) (again)
2021-10-09, by haftmann
tuned text;
2021-10-08, by wenzelm
recover NEWS from 78d1f73bbeaa;
2021-10-07, by wenzelm
save 90 MB by excluding rlwrap and thus perl;
2021-10-07, by wenzelm
save 45 MB by excluding rlwrap and thus perl;
2021-10-07, by wenzelm
NEWS;
2021-10-07, by wenzelm
clarified test of directories;
2021-10-07, by wenzelm
misc tuning for release;
2021-10-07, by wenzelm
merged
2021-10-07, by wenzelm
updated to kodkodi-1.5.7. with more robust/portable management of files and processes;
2021-10-07, by wenzelm
provide minisat-2.2.1 on all currently supported platforms, notably as external solver for Nitpick;
2021-10-07, by wenzelm
tuned message;
2021-10-07, by wenzelm
proper build on macOS;
2021-10-07, by wenzelm
build minisat, using recent fork from original sources;
2021-10-07, by wenzelm
proper platform_path for executables run from Java;
2021-10-07, by wenzelm
tuned message;
2021-10-07, by wenzelm
tuned;
2021-10-06, by wenzelm
tuned whitespace;
2021-10-06, by wenzelm
merged
2021-10-07, by desharna
added timeout to veriT
2021-10-07, by desharna
new notion of infinite sums in HOL-Analysis, ordering on complex numbers
2021-10-06, by eberlm
NEWS and CONTRIBUTORS
2021-10-07, by desharna
merged
2021-10-07, by desharna
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
less
more
|
(0)
-30000
-10000
-1920
+1920
tip