isabelle: Graph

useful lemma integral_less default tip
24 hours ago, by paulson
merged
28 hours ago, by desharna
removed unused parameter following f9908452b282
44 hours ago, by desharna
treat 'using X by meson' as 'by (meson X)' to avoid loss of polymorphism (cf. metis)
47 hours ago, by blanchet
fixed dodgy intro! attributes
2 days ago, by paulson
merged
3 days ago, by desharna
optimized facts traversal in TPTP translation
5 days ago, by desharna
optimized app_op_level selection in TPTP generation
5 days ago, by desharna
tuned trivial check in mirabelle_sledgehammer
6 days ago, by desharna
renamed run_action to run in Mirabelle.action record
6 days ago, by desharna
added spying of fact filtering timing
6 days ago, by desharna
tuned mirabelle_sledgehammer output
6 days ago, by desharna
added spying to Sledgehammer
6 days ago, by desharna
proper fact filter for dummy ATPs
6 days ago, by desharna
added syping of fact filtering time to sledgehammer
6 days ago, by desharna
removed unsynchronized references in mirabelle_sledgehammer
6 days ago, by desharna
tuned mirabelle_sledgehammer to have a single call to Synchronized.change per run
6 days ago, by desharna
updated to polyml-test-15c840d48c9a;
3 days ago, by wenzelm
some updates and clarification on Assumption.export_term;
6 days ago, by wenzelm
new theorem has_integral_UN
6 days ago, by paulson
updated to jdk-17.0.2+8;
6 days ago, by wenzelm
used elapsed time instead of cpu time in Mirabelle because the latter contain cpu time of all threads
7 days ago, by desharna
NEWS
7 days ago, by desharna
added Mirabelle option "-y" for dry run
7 days ago, by desharna
tuned garbage optimization
7 days ago, by desharna
added cpu time (in ms) to Mirabelle run_action output
9 days ago, by desharna
added Mirabelle option -r to randomize the goals before selection
9 days ago, by desharna
A new lemma about inverse image
10 days ago, by paulson
proper treatment of $let variables in symbol table in Sledgehammer
11 days ago, by desharna
removed unconditional TPTP symbol declaration for undefined_bool in sledgehammer
12 days ago, by desharna
merged
2 weeks ago, by desharna
split option "sledgehammer_atp_dest_dir" into "sledgehammer_atp_prob_dest_dir" and "sledgehammer_atp_proof_dest_dir"
2 weeks ago, by desharna
proper name mangling of "undefined" constants in Sledgehammer
2 weeks ago, by desharna
earlier availability of lifting
2 weeks ago, by haftmann
more correct transfer
2 weeks ago, by haftmann
merged
2 weeks ago, by desharna
proper abstraction of function variables when instantiating induction rules in Sledgehammer
2 weeks ago, by desharna
added lemma asympD
2 weeks ago, by desharna
added lemma
2 weeks ago, by nipkow
Some lemmas about continuous functions with integral zero
2 weeks ago, by paulson
merged
3 weeks ago, by desharna
added lemmas wf_imp_asym, wfP_imp_asymp, and wfP_imp_irreflp
3 weeks ago, by desharna
removed $ite from E 2.6 in THF format
3 weeks ago, by desharna
New and simplified theorems
3 weeks ago, by paulson
merged
3 weeks ago, by desharna
prefixed all mirabelle_sledgehammer output lines with sledgehammer output
3 weeks ago, by desharna
added lemma
4 weeks ago, by nipkow
Tiny additions inspired by Roth development
4 weeks ago, by paulson
allow general command transactions with presentation;
5 weeks ago, by wenzelm
more operations;
5 weeks ago, by wenzelm
clarified signature;
5 weeks ago, by wenzelm
tuned signature;
5 weeks ago, by wenzelm
support Gradle as alternative to Maven (again);
5 weeks ago, by wenzelm
tuned mirabelle command-line help message
5 weeks ago, by desharna
updated Mirabelle documentation
5 weeks ago, by desharna
proper documentation for induction_rules Sledgehammer option
5 weeks ago, by desharna
NEWS
5 weeks ago, by desharna
merged
5 weeks ago, by desharna
used TH1 for Leo-III in sledgehammer
5 weeks ago, by desharna
tuned run_sledgehammer and called it directly from Mirabelle
5 weeks ago, by desharna
exported Sledgehammer.launch_prover and use it in Mirabelle
5 weeks ago, by desharna
proper filtering inf induction rules in Mirabelle
5 weeks ago, by desharna
added nearly_all_facts_of_context and uniformized its usage in Sledgehammer and Mirabelle
6 weeks ago, by desharna
tuned ATP to use is_widely_irrelevant_const
6 weeks ago, by desharna
added support for initialization messages to Mirabelle
6 weeks ago, by desharna
tuned comment
5 weeks ago, by blanchet
support for JSON:API;
6 weeks ago, by wenzelm
support for Flarum server;
6 weeks ago, by wenzelm
tuned whitespace;
6 weeks ago, by wenzelm
tuned imports;
6 weeks ago, by wenzelm
tuned comments;
6 weeks ago, by wenzelm
clarified author names;
6 weeks ago, by wenzelm
clarified author names;
6 weeks ago, by wenzelm
merged
6 weeks ago, by wenzelm
more accurate names;
6 weeks ago, by wenzelm
more standard author_info;
6 weeks ago, by wenzelm
clarified author info and cluster nodes;
6 weeks ago, by wenzelm
more data integrity: name vs. address;
6 weeks ago, by wenzelm
clarified signature: more operations;
6 weeks ago, by wenzelm
clarified signature;
6 weeks ago, by wenzelm
tuned;
6 weeks ago, by wenzelm
more data integrity: name vs. address;
6 weeks ago, by wenzelm
tuned comments;
6 weeks ago, by wenzelm
merged
6 weeks ago, by desharna
tuned ATP to use fold_index
6 weeks ago, by desharna
tuned sledgehammer to use map_index
6 weeks ago, by desharna
merged
6 weeks ago, by wenzelm
more data integrity: name vs. address;
6 weeks ago, by wenzelm
misc tuning and clarification;
6 weeks ago, by wenzelm
clarified name;
6 weeks ago, by wenzelm
more mailing list content;
6 weeks ago, by wenzelm
more mailing list content;
6 weeks ago, by wenzelm
updated links;
6 weeks ago, by wenzelm
added Apache Commons Lang + Text: not particularly exciting, but provides useful things like org.apache.commons.text.StringEscapeUtils or org.apache.commons.text.diff;
6 weeks ago, by wenzelm
tuned ATP to use map_index
6 weeks ago, by desharna
removed obsolete RC tags;
6 weeks ago, by wenzelm
proper path;
6 weeks ago, by wenzelm
merged, resolving conflict in src/Doc/Implementation/Logic.thy;
6 weeks ago, by wenzelm
Added tag Isabelle2021-1 for changeset c2a2be496f35
6 weeks ago, by wenzelm
tuned; Isabelle2021-1
6 weeks ago, by wenzelm
proper ML types (amending 1aa92bc4d356);
7 weeks ago, by wenzelm
proper types for Scala.Fun instances (amending 1aa92bc4d356);
7 weeks ago, by wenzelm
proper syntax category;
7 weeks ago, by wenzelm
provide component naproche-20211211;
6 weeks ago, by wenzelm
merged
6 weeks ago, by wenzelm
more Mailman archives;
6 weeks ago, by wenzelm
more Mailman content;
6 weeks ago, by wenzelm
clarified signature;
6 weeks ago, by wenzelm
tuned metis to use map_index
7 weeks ago, by desharna
merged
7 weeks ago, by desharna
fixed HOL-TPTP
7 weeks ago, by desharna
tuned vars_of_iterm
7 weeks ago, by desharna
fixed TPTP generation of multi-arity expressions
7 weeks ago, by desharna
proper handling of Hilbert choice in TFX logics
8 weeks ago, by desharna
proper tptp_builtins
2 months ago, by desharna
reused Sledgehammer code to parse parameters of sledgehammer action in Mirabelle
2 months ago, by desharna
proper proxy for Hilbert choice in TPTP output
2 months ago, by desharna
proper polymorphism for TH1 format in Sledgehammer
2 months ago, by desharna
refactored $ite and $let configuration and added dummy_thf_reduced prover
2 months ago, by desharna
tuned TPTP file names generated by Sledgehammer
2 months ago, by desharna
tuned SMT-Lib file names generated by Mirabelle
2 months ago, by desharna
added support for higher-order SMT proof search in Sledgehammer
2 months ago, by desharna
separated FOOL from $ite/$let in TPTP output
2 months ago, by desharna
missing latex font
7 weeks ago, by nipkow
Rewrite: added links to docu, made more prominent
7 weeks ago, by nipkow
discontinued old-style {* verbatim *} tokens;
7 weeks ago, by wenzelm
tuned proof;
7 weeks ago, by wenzelm
isabelle update_cartouches;
7 weeks ago, by wenzelm
more symbolic latex_output via XML (using YXML within text);
7 weeks ago, by wenzelm
tuned signature: remove unused;
7 weeks ago, by wenzelm
prefer symbolic Latex.environment (typeset in Isabelle/Scala);
7 weeks ago, by wenzelm
tuned signature;
7 weeks ago, by wenzelm
clarified corner cases of syntax;
7 weeks ago, by wenzelm
clarified Parse.embedded_ml: follow documentation (8baf2e8b16e2);
7 weeks ago, by wenzelm
a slightly simpler proof
7 weeks ago, by paulson
provide component naproche-2d99afe5c349;
7 weeks ago, by wenzelm
merged
7 weeks ago, by wenzelm
Added tag Isabelle2021-1-RC5 for changeset 8baf2e8b16e2
7 weeks ago, by wenzelm
more documentation about Type/Const antiquotations;
7 weeks ago, by wenzelm
more documentation about document build options;
7 weeks ago, by wenzelm
address problems with launch4j and jdk-17 (see also 41d009462d3c, copy of 41d009462d3c);
8 weeks ago, by wenzelm
tuned --- fewer IDE warnings;
8 weeks ago, 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;
8 weeks ago, by wenzelm
added definitions multp{DM,HO} and corresponding lemmas
2 months ago, by desharna
added wfP_less to wellorder and wfP_less_multiset
2 months ago, by desharna
restored lemmas less_multiset{DM,HO} inadvertently changed by c256bba593f3
2 months ago, by desharna
merged
2 months ago, by desharna
added lemmas irreflp_{less,greater} to preorder and {trans,irrefl}_mult{,p} to Multiset
2 months ago, by desharna
redefined less_multiset to be based on multp
2 months ago, by desharna
added lemmas multp_code_eq_multp and multeqp_code_eq_reflclp_multp
2 months ago, by desharna
added lemmas multp_cancel, multp_cancel_add_mset, and multp_cancel_max
2 months ago, by desharna
added lemmas multp_implies_one_step, one_step_implies_multp, and subset_implies_multp
2 months ago, by desharna
added lemma wfP_multp
2 months ago, by desharna
added lemma mono_multp
2 months ago, by desharna
added Multiset.multp as predicate equivalent of Multiset.mult
2 months ago, by desharna
address problems with launch4j and jdk-17 (see also 41d009462d3c);
2 months ago, by wenzelm
more robust build on midrange hardware;
2 months ago, by wenzelm
clarified tests: omit somewhat pointless (unstable) results;
2 months ago, by wenzelm
proper fields for gnuplot (amending b614e3e4146a);
2 months ago, by wenzelm
tuned output;
2 months ago, by wenzelm
tuned;
2 months ago, by wenzelm
merged
2 months ago, by wenzelm
more robust build on midrange hardware (despite 67d6f1708ea4);
2 months ago, by wenzelm
Added tag Isabelle2021-1-RC4 for changeset 2336356d4180
2 months ago, by wenzelm
updated to polyml-5.9;
2 months ago, by wenzelm
NEWS on "isabelle mirabelle";
2 months ago, by wenzelm
tuned;
2 months ago, by wenzelm
clarified default for kodkod_scala;
2 months ago, by wenzelm
maintain option kodkod_scala within theory context, to allow local modification;
2 months ago, by wenzelm
NEWS for proper release;
2 months ago, by wenzelm
updated to flatlaf-1.6.4;
2 months ago, by wenzelm
avoid broken links: auxiliary files are not yet supported;
2 months ago, by wenzelm
option document_comment_latex supports e.g. Dagstuhl LIPIcs;
2 months ago, by wenzelm
more explicit type Latex.Tags;
2 months ago, by wenzelm
more uniform treatment of optional_argument for Latex elements;
2 months ago, by wenzelm
removed pointless 'text_cartouche' command: regular 'text' already supports cartouches;
2 months ago, by wenzelm
example: alternative document headings, based on more general document output markup;
2 months ago, by wenzelm
more general document output: enclosing markup is defined in user-space;
2 months ago, by wenzelm
clarified modules (see c299abcf7081);
2 months ago, by wenzelm
output for document commands like 'section', 'text' is defined in user-space, as part of the command transaction;
2 months ago, by wenzelm
clarified modules;
2 months ago, by wenzelm
tuned signature: more explicit types for presentation;
2 months ago, by wenzelm
more robust support for Windows line-endings;
2 months ago, by wenzelm
source positions for document markup commands, e.g. to retrieve PIDE markup in presentation;
2 months ago, by wenzelm
more compact data during presentation: Entity_Context.Theory_Export instead of full Export_Theory.Theory;
2 months ago, by wenzelm
clarified system option standard values: avoid oddities like "isabelle build -o document_output" producing directories named "true";
2 months ago, by wenzelm
more symbolic latex_output via XML (using YXML within text);
2 months ago, by wenzelm
proper enclose_name (amending e77c5bfca9aa);
2 months ago, by wenzelm
Latex.Output.latex_heading depends on option document_heading_prefix, e.g. relevant for Dagstuhl LIPIcs which prefers unaliased \section etc.;
2 months ago, by wenzelm
more symbolic latex_output via XML;
2 months ago, by wenzelm
clarified hook for Mirabelle (again): cover all 'theories' sections within ROOT (see also 9ead8d9be3ab);
2 months ago, by wenzelm
tuned;
2 months ago, by wenzelm
tuned;
2 months ago, by wenzelm
updated to verit-2021.06.2-rmx;
2 months ago, by wenzelm
clarified HTML_Context.theory_exports: prefer value-oriented parallelism;
2 months ago, by wenzelm
generate problems with correct logic for veriT
2 months ago, by fleury
more parallelism, at the cost of potential duplicates of make_thy;
2 months ago, by wenzelm
afford more parallelism for sessions (instead of theories in 5eac4b13d1f1): depend on disjoint data areas (notably base.session_theories in 2ad892ac749a);
2 months ago, by wenzelm
more interrupts;
2 months ago, by wenzelm
present only selected session theories (as in Isabelle2021), in contrast to 2bc24136bdeb, eb89b3a37826;
2 months ago, by wenzelm
tuned;
2 months ago, by wenzelm
clarified modules;
2 months ago, by wenzelm
tuned (see also e0d1d9203275);
2 months ago, by wenzelm
clarified signature;
2 months ago, by wenzelm
tuned;
2 months ago, by wenzelm
spelling;
2 months ago, by wenzelm
added asymp_{less,greater} to preorder and moved mult1_lessE out
2 months ago, by desharna
renamed multp_code_iff and multeqp_code_iff
2 months ago, by desharna
simplified mult_cancel_max and introduced orginal lemma as mult_cancel_max0
2 months ago, by desharna
renamed Multiset.multp and Multiset.multeqp
2 months ago, by desharna
added lemmas
2 months ago, by nipkow
merged
2 months ago, by wenzelm
tuned;
2 months ago, by wenzelm
removed redundant test (see also 86fac52c2795, a9fea3f11cc0);
2 months ago, by wenzelm
just one Presentation.State for all sessions: avoid duplication of already presented theories (very slow) and cached theory export (not very slow);
2 months ago, by wenzelm
proper version;
2 months ago, by wenzelm
back to Z3 4.4.0pre for all platforms except arm64-linux: avoid failure e.g. in Padic_Ints (AFP/7a2522dce834);
2 months ago, by wenzelm
less ambitious parallelism: more direct read/write saves overall heap space and GC time;
2 months ago, by wenzelm
slightly faster XML output: avoid too much regrowing of StringBuilder;
2 months ago, by wenzelm
updated NEWS: arm64-linux support is almost complete;
2 months ago, by wenzelm
update z3-4.4.0pre-3 to z3-4.4.1, which happens to have an arm64_linux executable in Debian 9;
2 months ago, by wenzelm
more material for HOL-Analysis.Infinite_Sum
2 months ago, by Manuel Eberl
more symbolic latex_output via XML;
2 months ago, by wenzelm
clarified signature;
2 months ago, by wenzelm
updated to polyml-5.9-610a153b941d -- close to final;
2 months ago, by wenzelm
tuned signature (again): latex_output is likely to depend on context;
2 months ago, by wenzelm
more symbolic latex output;
2 months ago, by wenzelm
tuned signature;
2 months ago, by wenzelm
symbolic latex_output via XML, interpreted in Isabelle/Scala;
2 months ago, by wenzelm
tuned signature;
2 months ago, by wenzelm
clarified signature;
2 months ago, by wenzelm
clarified signature;
2 months ago, by wenzelm
clarified signature: more privacy;
2 months ago, by wenzelm
tuned output --- less redundancy;
2 months ago, by wenzelm
tuned whitespace;
2 months ago, by wenzelm
clarified signature: Latex.Output as parameter to Document_Build.Engine;
2 months ago, by wenzelm
proper detection of ARM platform variants;
2 months ago, by wenzelm
back to post-release mode;
2 months ago, by wenzelm
updated for release;
2 months ago, by wenzelm
Added tag Isabelle2021-1-RC3 for changeset 2b212c8138a5
2 months ago, by wenzelm