isabelle: Graph

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