| 4 months ago |
wenzelm |
clarified solr_data directory, provided via settings;
|
file |
diff |
annotate
|
| 4 months ago |
wenzelm |
clarified names;
|
file |
diff |
annotate
|
| 4 months ago |
wenzelm |
more NEWS + CONTRIBUTORS;
|
file |
diff |
annotate
|
| 4 months ago |
paulson |
fixed a typo
|
file |
diff |
annotate
|
| 4 months ago |
haftmann |
corrected
|
file |
diff |
annotate
|
| 4 months ago |
Lukas Bartl |
Rename "suggest_of" to "instantiate"
|
file |
diff |
annotate
|
| 4 months ago |
wenzelm |
discontinue old / inaccurate show_brackets (see also a4f09493d929 and ca9f5dbab880);
|
file |
diff |
annotate
|
| 4 months ago |
wenzelm |
proper NEWS section;
|
file |
diff |
annotate
|
| 4 months ago |
wenzelm |
merged
|
file |
diff |
annotate
|
| 4 months ago |
wenzelm |
tuned NEWS;
|
file |
diff |
annotate
|
| 4 months ago |
wenzelm |
updated Ubuntu versions;
|
file |
diff |
annotate
|
| 4 months ago |
wenzelm |
merged
|
file |
diff |
annotate
|
| 4 months ago |
wenzelm |
update NEWS / documentation / descriptions for Phorge (formerly Phabricator);
|
file |
diff |
annotate
|
| 4 months ago |
haftmann |
optionally use shift operations on target numerals for efficient execution
|
file |
diff |
annotate
|
| 4 months ago |
wenzelm |
rebuild E 3.1 on Windows/Cygwin, with patch for proper interrupts;
|
file |
diff |
annotate
|
| 4 months ago |
wenzelm |
misc tuning and updates for release;
|
file |
diff |
annotate
|
| 4 months ago |
wenzelm |
tuned NEWS;
|
file |
diff |
annotate
|
| 4 months ago |
haftmann |
refined syntax for code_reserved
|
file |
diff |
annotate
|
| 4 months ago |
wenzelm |
revert changeset 2f98e3c4592c: avoid conflict with low-level \<^latex> markup;
|
file |
diff |
annotate
|
| 4 months ago |
wenzelm |
more LaTeX markup;
|
file |
diff |
annotate
|
| 4 months ago |
wenzelm |
clarified LaTeX presentation: more specific keywords;
|
file |
diff |
annotate
|
| 5 months ago |
wenzelm |
more syntax bundles, e.g. to explore terms without notation;
|
file |
diff |
annotate
|
| 5 months ago |
wenzelm |
syntax translations now work in a local theory context;
|
file |
diff |
annotate
|
| 5 months ago |
wenzelm |
proper bundle binomial_syntax;
|
file |
diff |
annotate
|
| 5 months ago |
wenzelm |
more LaTeX markup for printed entities;
|
file |
diff |
annotate
|
| 5 months ago |
wenzelm |
NEWS;
|
file |
diff |
annotate
|
| 5 months ago |
wenzelm |
prefer Term.variant_bounds: bounds vs. frees, no attempt at consts;
|
file |
diff |
annotate
|
| 5 months ago |
wenzelm |
clarified 'unbundle' polarity, according to algebraic group laws;
|
file |
diff |
annotate
|
| 5 months ago |
wenzelm |
merged
|
file |
diff |
annotate
|
| 5 months ago |
wenzelm |
Output_Dockable: show search results as tree view;
|
file |
diff |
annotate
|
| 5 months ago |
nipkow |
renamed Discrete -> Discrete_Functions to avoid name clashes;
|
file |
diff |
annotate
|
| 6 months ago |
wenzelm |
more NEWS;
|
file |
diff |
annotate
|
| 6 months ago |
wenzelm |
less ambitious selection;
|
file |
diff |
annotate
|
| 6 months ago |
wenzelm |
clarified mouse selection, avoid conflict of double-click with single-click (follow hyperlink);
|
file |
diff |
annotate
|
| 6 months ago |
wenzelm |
more NEWS;
|
file |
diff |
annotate
|
| 6 months ago |
wenzelm |
misc tuning and clarification: Doc.Entry supports both plain files and pdf documents;
|
file |
diff |
annotate
|
| 6 months ago |
wenzelm |
support incremental isabelle.select-structure --- like select-block, but based on selection instead of caret;
|
file |
diff |
annotate
|
| 6 months ago |
wenzelm |
more NEWS;
|
file |
diff |
annotate
|
| 6 months ago |
wenzelm |
support Isabelle/jEdit action isabelle.select_structure;
|
file |
diff |
annotate
|
| 6 months ago |
wenzelm |
tuned NEWS;
|
file |
diff |
annotate
|
| 6 months ago |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| 6 months ago |
wenzelm |
misc tuning and clarification;
|
file |
diff |
annotate
|
| 6 months ago |
wenzelm |
clarified section structure;
|
file |
diff |
annotate
|
| 6 months ago |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| 6 months ago |
blanchet |
variable instantiation in Sledgehammer and Metis
|
file |
diff |
annotate
|
| 6 months ago |
wenzelm |
prefer rewrite_term_yoyo for improved performance and occasionally better results (conforming to Ast.normalize);
|
file |
diff |
annotate
|
| 6 months ago |
wenzelm |
print type constraints for consts with mixfix syntax;
|
file |
diff |
annotate
|
| 7 months ago |
wenzelm |
show_consts_markup is enabled by default;
|
file |
diff |
annotate
|
| 7 months ago |
wenzelm |
allow type constraints for const_syntax;
|
file |
diff |
annotate
|
| 7 months ago |
wenzelm |
tuned NEWS;
|
file |
diff |
annotate
|
| 7 months ago |
wenzelm |
more NEWS;
|
file |
diff |
annotate
|
| 7 months ago |
wenzelm |
more NEWS;
|
file |
diff |
annotate
|
| 7 months ago |
wenzelm |
more syntax bundles;
|
file |
diff |
annotate
|
| 7 months ago |
wenzelm |
more syntax bundles;
|
file |
diff |
annotate
|
| 7 months ago |
wenzelm |
clarified bundles for list syntax;
|
file |
diff |
annotate
|
| 7 months ago |
wenzelm |
more inner-syntax markup;
|
file |
diff |
annotate
|
| 7 months ago |
wenzelm |
support for pretty blocks that are "open" and thus have no impact on formatting, only on markup;
|
file |
diff |
annotate
|
| 7 months ago |
wenzelm |
ML antiquotation for formally-checked bundle names;
|
file |
diff |
annotate
|
| 7 months ago |
wenzelm |
first-class support for "unbundle no foobar_syntax" -- avoid redundant "bundle no_foobar_syntax" definitions;
|
file |
diff |
annotate
|
| 7 months ago |
wenzelm |
misc tuning;
|
file |
diff |
annotate
|
| 7 months ago |
wenzelm |
clarified syntax for opening bundles;
|
file |
diff |
annotate
|
| 7 months ago |
wenzelm |
merged
|
file |
diff |
annotate
|
| 7 months ago |
wenzelm |
provide 'open_bundle' command;
|
file |
diff |
annotate
|
| 7 months ago |
wenzelm |
more NEWS;
|
file |
diff |
annotate
|
| 7 months ago |
Fabian Huch |
NEWS and CONTRIBUTORS;
|
file |
diff |
annotate
|
| 7 months ago |
wenzelm |
clarified inner-syntax markup, notably for enumerations: prefer "notation=mixfix" over "entity" via 'syntax_consts' (see also 70076ba563d2);
|
file |
diff |
annotate
|
| 8 months ago |
wenzelm |
clarified internal tool output: prefer Pretty.pure_string_of over manipulation of print_mode;
|
file |
diff |
annotate
|
| 8 months ago |
wenzelm |
tuned signature: more operations;
|
file |
diff |
annotate
|
| 8 months ago |
wenzelm |
drop pointless print_mode operations Output.output / Output.escape;
|
file |
diff |
annotate
|
| 8 months ago |
wenzelm |
clarified print mode "latex": no longer impact Output/Markup/Pretty operations;
|
file |
diff |
annotate
|
| 8 months ago |
wenzelm |
NEWS: value-oriented Pretty.T;
|
file |
diff |
annotate
|
| 8 months ago |
wenzelm |
proper formal sections;
|
file |
diff |
annotate
|
| 8 months ago |
wenzelm |
more NEWS;
|
file |
diff |
annotate
|
| 8 months ago |
wenzelm |
NEWS and documentation;
|
file |
diff |
annotate
|
| 9 months ago |
wenzelm |
adapt and activate congprocs examples, following the current Simplifier implementation;
|
file |
diff |
annotate
|
| 9 months ago |
wenzelm |
more direct access to Simplifier.mk_cong, to avoid odd Simpdata.mk_meta_cong seen in the wild;
|
file |
diff |
annotate
|
| 9 months ago |
wenzelm |
support for congprocs in the Simplifier, closely following Norbert Schirmer et-al, but with only one "simproc" name space and "simproc_setup" command / ML antiquotation;
|
file |
diff |
annotate
|
| 10 months ago |
desharna |
added lemmas wfp_on_antimono_stronger and wf_on_antimono_stronger
|
file |
diff |
annotate
|
| 10 months ago |
Fabian Huch |
NEWS and CONTRIBUTORS;
|
file |
diff |
annotate
|
| 10 months ago |
paulson |
NEWS: totalisation of ln
|
file |
diff |
annotate
|
| 10 months ago |
desharna |
added lemma image_mset_diff_if_inj
|
file |
diff |
annotate
|
| 10 months ago |
desharna |
added lemma minus_add_mset_if_not_in_lhs[simp]
|
file |
diff |
annotate
|
| 10 months ago |
wenzelm |
NEWS;
|
file |
diff |
annotate
|
| 10 months ago |
haftmann |
moved transitional theory Divides to HOL-Library
|
file |
diff |
annotate
|
| 11 months ago |
desharna |
removed lemma wellorder.wfP_less
|
file |
diff |
annotate
|
| 11 months ago |
desharna |
fixed NEWS
|
file |
diff |
annotate
|
| 11 months ago |
desharna |
renamed lemmas
|
file |
diff |
annotate
|
| 11 months ago |
desharna |
renamed theorems
|
file |
diff |
annotate
|
| 11 months ago |
desharna |
renamed theorems
|
file |
diff |
annotate
|
| 11 months ago |
desharna |
renamed theorems
|
file |
diff |
annotate
|
| 11 months ago |
desharna |
renamed lemmas
|
file |
diff |
annotate
|
| 11 months ago |
wenzelm |
merged
|
file |
diff |
annotate
|
| 12 months ago |
wenzelm |
more documentation on "isabelle build -H" and underlying system registry tables "host" and "cluster";
|
file |
diff |
annotate
|
| 13 months ago |
wenzelm |
back to post-release mode -- after fork point;
|
file |
diff |
annotate
|
| 13 months ago |
wenzelm |
avoid Scala if-expressions and thus make it work both for -new-syntax or -old-syntax;
|
file |
diff |
annotate
|
| 13 months ago |
desharna |
documented new syntax for fBall and fBex
|
file |
diff |
annotate
|
| 13 months ago |
wenzelm |
misc tuning for release;
|
file |
diff |
annotate
|
| 13 months ago |
Fabian Huch |
update NEWS;
|
file |
diff |
annotate
|
| 13 months ago |
desharna |
merged
|
file |
diff |
annotate
|
| 13 months ago |
desharna |
added lemma wfp_on_image and author name to theory
|
file |
diff |
annotate
|
| 13 months ago |
wenzelm |
merged
|
file |
diff |
annotate
|
| 13 months ago |
wenzelm |
tuned NEWS;
|
file |
diff |
annotate
|
| 13 months ago |
paulson |
New material and a bit of refactoring
|
file |
diff |
annotate
|
| 13 months ago |
desharna |
merged
|
file |
diff |
annotate
|
| 13 months ago |
desharna |
renamed lemma wfP_iff_ex_minimal to wfp_iff_ex_minimal
|
file |
diff |
annotate
|
| 13 months ago |
wenzelm |
misc tuning for release;
|
file |
diff |
annotate
|
| 13 months ago |
wenzelm |
merged;
|
file |
diff |
annotate
|
| 13 months ago |
wenzelm |
NEWS for "isabelle go_setup";
|
file |
diff |
annotate
|
| 13 months ago |
desharna |
added lemmas wfp_on_inv_imagep, wfp_on_if_convertible_to_wfp_on, and wf_on_if_convertible_to_wf_on
|
file |
diff |
annotate
|
| 13 months ago |
desharna |
merged
|
file |
diff |
annotate
|
| 13 months ago |
desharna |
added lemma wf_on_iff_wf
|
file |
diff |
annotate
|
| 13 months ago |
wenzelm |
MLton lacks arm64-linux (see also 84f2d481d6d7);
|
file |
diff |
annotate
|
| 13 months ago |
nipkow |
documented running time function framework by Jonas Stahl
|
file |
diff |
annotate
|
| 13 months ago |
desharna |
redefined wf as an abbreviation for "wf_on UNIV"
|
file |
diff |
annotate
|
| 13 months ago |
desharna |
tuned NEWS
|
file |
diff |
annotate
|
| 14 months ago |
desharna |
redefined wfP as an abbreviation for "wfp_on UNIV"
|
file |
diff |
annotate
|
| 13 months ago |
desharna |
merged
|
file |
diff |
annotate
|
| 14 months ago |
desharna |
added lemma wellorder.wfp_on_less[simp]
|
file |
diff |
annotate
|
| 14 months ago |
wenzelm |
suppress arm64-darwin, which does not support "-codegen native" (required for AFP/PAC_Checker);
|
file |
diff |
annotate
|
| 14 months ago |
wenzelm |
update to mlton-20210117-2, which covers x86_64-linux, x86_64-darwin, arm64-darwin;
|
file |
diff |
annotate
|
| 14 months ago |
desharna |
merged
|
file |
diff |
annotate
|
| 14 months ago |
desharna |
try proof method "order" in Sledgehammer's proof reconstruction
|
file |
diff |
annotate
|
| 14 months ago |
desharna |
added Mirabelle action "order"
|
file |
diff |
annotate
|
| 14 months ago |
desharna |
renamed lemma antisymp_on_reflcp to antisymp_on_reflclp
|
file |
diff |
annotate
|
| 14 months ago |
desharna |
added lemma order_reflclp_if_transp_and_asymp
|
file |
diff |
annotate
|
| 14 months ago |
desharna |
added lemmas antisym_on_reflcl_if_asym_on and antisymp_on_reflclp_if_asymp_on
|
file |
diff |
annotate
|
| 14 months ago |
Manuel Eberl |
more general definition of meromorphicity; Weierstraß factorisation theorem
|
file |
diff |
annotate
|
| 14 months ago |
desharna |
added alias wfp for wfP
|
file |
diff |
annotate
|
| 14 months ago |
desharna |
added lemmas wf_on_antimono, wf_on_antimono_strong, wfp_on_antimono, wfp_on_antimono_strong, wf_on_subset, and wfp_on_subset
|
file |
diff |
annotate
|
| 14 months ago |
desharna |
added lemmas wfP_iff_ex_minimal, wf_iff_ex_minimal, wf_onE_pf, wf_onI_pf, wf_on_iff_ex_minimal, and wfp_on_iff_ex_minimal
|
file |
diff |
annotate
|
| 14 months ago |
desharna |
added definitions wf_on and wfp_on as restricted versions of wf and wfP respectively
|
file |
diff |
annotate
|
| 14 months ago |
desharna |
added lemmas antisymp_on_image, asymp_on_image, irreflp_on_image, reflp_on_image, symp_on_image, totalp_on_image, and transp_on_image
|
file |
diff |
annotate
|
| 14 months ago |
wenzelm |
update NEWS + CONTRIBUTORS for release;
|
file |
diff |
annotate
|
| 14 months ago |
wenzelm |
update NEWS;
|
file |
diff |
annotate
|
| 14 months ago |
desharna |
added lemmas reflclp_(less|greater)_eq[simp], rtranclp_(less|greater)_eq[simp], and tranclp_(less|greater|less_eq|greater_eq)[simp]
|
file |
diff |
annotate
|
| 14 months ago |
wenzelm |
revised NEWS: OCaml / OPAM appears to be fine on arm64-linux, e.g. Ubuntu 22.04;
|
file |
diff |
annotate
|
| 14 months ago |
wenzelm |
update to current long-term-support version dotnet-8.0.x;
|
file |
diff |
annotate
|
| 14 months ago |
wenzelm |
misc tuning for release;
|
file |
diff |
annotate
|
| 14 months ago |
wenzelm |
merged
|
file |
diff |
annotate
|
| 14 months ago |
wenzelm |
update NEWS;
|
file |
diff |
annotate
|
| 14 months ago |
desharna |
added lemmas rtranclp_ident_if_reflp_and_transp and tranclp_ident_if_transp
|
file |
diff |
annotate
|
| 14 months ago |
wenzelm |
official support for arm64-linux, despite a few missing tools;
|
file |
diff |
annotate
|
| 14 months ago |
Fabian Huch |
update NEWS, following 0d7c7fe65638;
|
file |
diff |
annotate
|
| 14 months ago |
wenzelm |
tuned NEWS, see also c62003e05e46;
|
file |
diff |
annotate
|
| 14 months ago |
wenzelm |
update NEWS, following ea1913c953ef;
|
file |
diff |
annotate
|
| 14 months ago |
wenzelm |
tuned whitespace according to jEdit mode parameters ":wrap=hard:maxLineLen=72:";
|
file |
diff |
annotate
|
| 14 months ago |
wenzelm |
more explicit NEWS (see 3648e9c88d0c);
|
file |
diff |
annotate
|
| 14 months ago |
wenzelm |
NEWS for a53287d9add3, 3e30ca77ccfe;
|
file |
diff |
annotate
|
| 14 months ago |
Fabian Huch |
add option for unify trace (now disabled by default as printing is excessive and rarely used);
|
file |
diff |
annotate
|
| 14 months ago |
blanchet |
new less ad hoc implementation of the 'moura' tactic for skolemization
|
file |
diff |
annotate
|
| 15 months ago |
desharna |
added lemmas relpowp_left_unique and relpow_left_unique
|
file |
diff |
annotate
|
| 15 months ago |
desharna |
added lemmas relpowp_right_unique and relpow_right_unique
|
file |
diff |
annotate
|
| 15 months ago |
wenzelm |
clarified default "isabelle build -j0 -H";
|
file |
diff |
annotate
|
| 15 months ago |
desharna |
merged
|
file |
diff |
annotate
|
| 15 months ago |
desharna |
added lemmas relpow_trans[trans] and relpowp_trans[trans]
|
file |
diff |
annotate
|
| 15 months ago |
paulson |
the syntax of Lebesgue integrals (LINT, LBINT, ∫, etc.) now requires parentheses
|
file |
diff |
annotate
|
| 15 months ago |
paulson |
NEWS: corrected the definition of convexity of functions
|
file |
diff |
annotate
|
| 15 months ago |
desharna |
added lemmas Multiset.transp_on_multp and Multiset.trans_on_mult
|
file |
diff |
annotate
|
| 16 months ago |
wenzelm |
update to llncs-2.23;
|
file |
diff |
annotate
|
| 16 months ago |
haftmann |
consolidated lemma name
|
file |
diff |
annotate
|
| 17 months ago |
haftmann |
compactified specification of type class parity
|
file |
diff |
annotate
|
| 17 months ago |
wenzelm |
removed obsolete/broken isabelle_scala_script wrapper (see also abf9fcfa65cf);
|
file |
diff |
annotate
|
| 17 months ago |
wenzelm |
provide src/Tools/Demo as example for system component with Isabelle/Scala tool;
|
file |
diff |
annotate
|
| 18 months ago |
wenzelm |
NEWS;
|
file |
diff |
annotate
|
| 18 months ago |
desharna |
NEWS
|
file |
diff |
annotate
|
| 18 months ago |
haftmann |
more specific name for type class
|
file |
diff |
annotate
|
| 18 months ago |
wenzelm |
more NEWS;
|
file |
diff |
annotate
|
| 18 months ago |
haftmann |
slightly less technical formulation of very specific type class
|
file |
diff |
annotate
|
| 18 months ago |
haftmann |
explicit type class for discrete linordered semidoms
|
file |
diff |
annotate
|
| 18 months ago |
Fabian Huch |
NEWS and CONTRIBUTORS;
|
file |
diff |
annotate
|
| 19 months ago |
wenzelm |
update documentation on simproc_setup;
|
file |
diff |
annotate
|
| 19 months ago |
wenzelm |
proper morphism;
|
file |
diff |
annotate
|
| 19 months ago |
wenzelm |
simprocs may be distinguished via 'identifier': only works for ML antiquotation (see also 13252110a6fe);
|
file |
diff |
annotate
|
| 19 months ago |
wenzelm |
added ML antiquotation "simproc_setup";
|
file |
diff |
annotate
|
| 19 months ago |
wenzelm |
more NEWS;
|
file |
diff |
annotate
|
| 19 months ago |
wenzelm |
more NEWS;
|
file |
diff |
annotate
|
| 19 months ago |
wenzelm |
tuned structure;
|
file |
diff |
annotate
|
| 19 months ago |
wenzelm |
distinguish proper interrupts from Poly/ML RTS breakdown;
|
file |
diff |
annotate
|
| 19 months ago |
desharna |
NEWS
|
file |
diff |
annotate
|
| 19 months ago |
wenzelm |
more NEWS;
|
file |
diff |
annotate
|
| 19 months ago |
wenzelm |
explicitly reject 'handle' with catch-all patterns;
|
file |
diff |
annotate
|
| 20 months ago |
wenzelm |
tuned NEWS;
|
file |
diff |
annotate
|
| 20 months ago |
wenzelm |
NEWS;
|
file |
diff |
annotate
|
| 20 months ago |
wenzelm |
merged
|
file |
diff |
annotate
|
| 20 months ago |
wenzelm |
minimal documentation for build cluster support;
|
file |
diff |
annotate
|
| 21 months ago |
wenzelm |
clarified command arguments: optionally restrict to given theories (from theory loader);
|
file |
diff |
annotate
|
| 21 months ago |
wenzelm |
added Isar command 'print_context_tracing';
|
file |
diff |
annotate
|
| 21 months ago |
wenzelm |
back to post-release mode -- after fork point;
|
file |
diff |
annotate
|
| 21 months ago |
wenzelm |
update to polyml-219e0a248f70, with more robust support for ARM64;
|
file |
diff |
annotate
|
| 21 months ago |
wenzelm |
prefer Output.writeln for theory "results", as opposed to Output.state for genuine proof states (see f8c412a45af8, c668735fb8b5, ecf80e37ed1a);
|
file |
diff |
annotate
|
| 22 months ago |
wenzelm |
tuned NEWS: emphasize "isabelle build" add-ons;
|
file |
diff |
annotate
|
| 22 months ago |
wenzelm |
added option -A for AFP root, following "isabelle sync";
|
file |
diff |
annotate
|
| 22 months ago |
wenzelm |
update for release;
|
file |
diff |
annotate
|
| 22 months ago |
paulson |
X = trivial_topology rather than topspace X = {}
|
file |
diff |
annotate
|
| 22 months ago |
paulson |
News update referring to Analysis
|
file |
diff |
annotate
|
| 22 months ago |
wenzelm |
more NEWS;
|
file |
diff |
annotate
|
| 22 months ago |
wenzelm |
more NEWS;
|
file |
diff |
annotate
|
| 22 months ago |
wenzelm |
NEWS;
|
file |
diff |
annotate
|
| 22 months ago |
wenzelm |
revert ineffective b04ac8a017b2: etc/settings of polyml components needs to be changed as well;
|
file |
diff |
annotate
|
| 22 months ago |
wenzelm |
ML_system_apple=false for more stability;
|
file |
diff |
annotate
|
| 22 months ago |
wenzelm |
update to stack-2.9.3 with support for arm64-linux;
|
file |
diff |
annotate
|
| 22 months ago |
wenzelm |
clarified signature, with subtle change of semantics (amending 8b5a2e4b16d4);
|
file |
diff |
annotate
|
| 22 months ago |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| 22 months ago |
paulson |
NEWS tweak
|
file |
diff |
annotate
|
| 22 months ago |
desharna |
add proof method "order" to command "try0"
|
file |
diff |
annotate
|
| 23 months ago |
kleing |
optional description in Eisbach "method" command;
|
file |
diff |
annotate
|
| 23 months ago |
blanchet |
disable 'falsify' and 'abduce' in Sledgehammer by default, since they don't seem to be very useful in practice
|
file |
diff |
annotate
|
| 23 months ago |
wenzelm |
updated for release;
|
file |
diff |
annotate
|
| 23 months ago |
wenzelm |
tuned NEWS;
|
file |
diff |
annotate
|
| 23 months ago |
wenzelm |
more realistic factor;
|
file |
diff |
annotate
|
| 23 months ago |
desharna |
added lemma ffUnion_fsubset_iff
|
file |
diff |
annotate
|
| 23 months ago |
paulson |
NEWS: Announcing the metric space material
|
file |
diff |
annotate
|
| 23 months ago |
wenzelm |
more NEWS;
|
file |
diff |
annotate
|
| 23 months ago |
wenzelm |
tuned NEWS;
|
file |
diff |
annotate
|
| 23 months ago |
wenzelm |
NEWS;
|
file |
diff |
annotate
|
| 23 months ago |
desharna |
NEWS
|
file |
diff |
annotate
|
| 24 months ago |
desharna |
NEWS
|
file |
diff |
annotate
|
| 2023-05-10 |
desharna |
added lemmas transp_on_multpHO and transp_multpHO
|
file |
diff |
annotate
|
| 2023-05-09 |
desharna |
added lemmas Finite_Set.bex_(min|max)_element_with_property and reordered assumptions of Finite_Set.bex_(min|max)_element
|
file |
diff |
annotate
|
| 2023-05-08 |
desharna |
merged
|
file |
diff |
annotate
|
| 2023-05-08 |
desharna |
added lemma asymp_on_multpHO
|
file |
diff |
annotate
|
| 2023-05-08 |
desharna |
added lemmas multpHO_iff_set_mset_lessHO_set_mset and multpHO_minus_inter_minus_inter_iff
|
file |
diff |
annotate
|
| 2023-05-08 |
desharna |
added lemmas count_minus_inter_lt_count_minus_inter_iff and minus_inter_eq_minus_inter_iff
|
file |
diff |
annotate
|
| 2023-05-08 |
desharna |
added lemma multpHO_implies_one_step_strong
|
file |
diff |
annotate
|
| 2023-05-02 |
wenzelm |
more standard name bindings (amending 5bf71b4da706): avoid odd full_name like "Orderings.class.Orderings.preorder.of_class.intro" with many redundant name space accesses;
|
file |
diff |
annotate
|
| 2023-04-27 |
blanchet |
made 'primcorec' more robust
|
file |
diff |
annotate
|
| 2023-04-22 |
wenzelm |
provide ML antiquotation "if_none": non-strict version of "the_default";
|
file |
diff |
annotate
|
| 2023-04-18 |
wenzelm |
update NEWS: Sortset and Termset turned out to be counter productive, Ord_List.union is much lighter;
|
file |
diff |
annotate
|
| 2023-04-13 |
desharna |
added lemmas multpHO_repeat_mset_repeat_mset[simp] and multpHO_double_double[simp]
|
file |
diff |
annotate
|
| 2023-04-12 |
desharna |
added lemma multp_image_mset_image_msetI
|
file |
diff |
annotate
|
| 2023-04-10 |
wenzelm |
more NEWS;
|
file |
diff |
annotate
|
| 2023-04-10 |
wenzelm |
clarified NEWS;
|
file |
diff |
annotate
|
| 2023-04-10 |
wenzelm |
NEWS;
|
file |
diff |
annotate
|
| 2023-04-08 |
wenzelm |
use "rsync --secluded-args" by default, discontinue obsolete option -P of sync tools;
|
file |
diff |
annotate
|
| 2023-04-08 |
wenzelm |
clarified underlying SSH session of "isabelle hg_sync" and "isabelle sync";
|
file |
diff |
annotate
|
| 2023-03-27 |
wenzelm |
NEWS;
|
file |
diff |
annotate
|
| 2023-03-20 |
desharna |
reordered assumption and tuned proof of Multiset.bex_least_element and Multiset.bex_greatest_element
|
file |
diff |
annotate
|
| 2023-03-20 |
desharna |
added lemmas Finite_Set.bex_least_element and Finite_Set.bex_greatest_element
|
file |
diff |
annotate
|
| 2023-03-20 |
desharna |
added lemmas Finite_Set.bex_min_element and Finite_Set.bex_max_element
|
file |
diff |
annotate
|
| 2023-03-20 |
desharna |
reversed import dependency between Relation and Finite_Set; and move theorems around
|
file |
diff |
annotate
|
| 2023-03-20 |
wenzelm |
clarified operations for ML object sizes;
|
file |
diff |
annotate
|
| 2023-03-17 |
desharna |
added lemma multp_repeat_mset_repeat_msetI
|
file |
diff |
annotate
|
| 2023-03-16 |
wenzelm |
merged
|
file |
diff |
annotate
|
| 2023-03-16 |
wenzelm |
more thorough treatment of build prefs, guarded by system option "build_through": avoid accidental rebuild of HOL etc.;
|
file |
diff |
annotate
|
| 2023-03-16 |
wenzelm |
clarified build options;
|
file |
diff |
annotate
|
| 2023-03-16 |
nipkow |
merge conflict
|
file |
diff |
annotate
|
| 2023-03-16 |
nipkow |
unified function update and map update syntaxes
|
file |
diff |
annotate
|
| 2023-03-15 |
nipkow |
map update syntax
|
file |
diff |
annotate
|
| 2023-03-11 |
wenzelm |
NEWS;
|
file |
diff |
annotate
|
| 2023-03-07 |
wenzelm |
renamed "isabelle build_docker" to "isabelle docker_build" (unrelated to "isabelle build");
|
file |
diff |
annotate
|
| 2023-03-07 |
wenzelm |
renamed "isabelle log" to "isabelle build_log";
|
file |
diff |
annotate
|
| 2023-03-05 |
wenzelm |
clarified protocol for "verbose" messages;
|
file |
diff |
annotate
|
| 2023-03-02 |
wenzelm |
merged
|
file |
diff |
annotate
|
| 2023-03-02 |
wenzelm |
clarified names;
|
file |
diff |
annotate
|
| 2023-03-02 |
paulson |
merged
|
file |
diff |
annotate
|
| 2023-02-28 |
paulson |
Imported a theorem about Infinite_Sum. Importing this theory a bit earlier is causing syntactic ambiguities with Infinite_Set_Sum however; no_notation needed
|
file |
diff |
annotate
|
| 2023-03-01 |
blanchet |
adopt terminology suggested by Larry Paulson
|
file |
diff |
annotate
|
| 2023-03-01 |
blanchet |
updated documentation
|
file |
diff |
annotate
|
| 2023-02-23 |
nipkow |
Map.empty no longer output abbreviation; %_. None is shorter and requires no explanation
|
file |
diff |
annotate
|
| 2023-02-23 |
desharna |
added lemmas strict_subset_implies_multpDM and strict_subset_implies_multpHO
|
file |
diff |
annotate
|
| 2023-02-23 |
desharna |
added lemma multpDM_plus_plusI[simp]
|
file |
diff |
annotate
|
| 2023-02-23 |
desharna |
added lemmas multpDM_mono_strong and multpHO_mono_strong
|
file |
diff |
annotate
|
| 2023-02-20 |
nipkow |
merged
|
file |
diff |
annotate
|
| 2023-02-20 |
nipkow |
Backed out changeset 1fde0e4fd791
|
file |
diff |
annotate
|
| 2023-02-18 |
desharna |
added lemmas asymp_not_liftable_to_multpHO and asymp_multpHO
|
file |
diff |
annotate
|
| 2023-02-15 |
blanchet |
added refute mode to Sledgehammer to find 'counterexamples'
|
file |
diff |
annotate
|
| 2023-02-14 |
nipkow |
merged
|
file |
diff |
annotate
|
| 2023-02-14 |
nipkow |
Map.map_of movement
|
file |
diff |
annotate
|
| 2023-02-13 |
blanchet |
updated NEWS
|
file |
diff |
annotate
|
| 2023-01-30 |
wenzelm |
observe option "show_states" in headless server (see also 951abf9db857);
|
file |
diff |
annotate
|
| 2023-01-27 |
desharna |
added lemma multpHO_plus_plus[simp]
|
file |
diff |
annotate
|
| 2023-01-24 |
desharna |
merged
|
file |
diff |
annotate
|
| 2023-01-23 |
desharna |
added lemma irreflp_on_multpHO[simp]
|
file |
diff |
annotate
|
| 2023-01-23 |
desharna |
added lemmas totalp_on_multpDM, totalp_multpDM, totalp_on_multpHO, and totalp_multpHO
|
file |
diff |
annotate
|
| 2023-01-24 |
haftmann |
generalized theory name: euclidean division denotes one particular division definition on integers
|
file |
diff |
annotate
|
| 2023-01-23 |
desharna |
added lemmas total_on_mult, total_mult, totalp_on_multp, and totalp_multp
|
file |
diff |
annotate
|
| 2023-01-23 |
desharna |
proper name for lemma totalp_on_total_on_eq
|
file |
diff |
annotate
|
| 2023-01-19 |
paulson |
HOL/Library/BigO is obsolete
|
file |
diff |
annotate
|
| 2023-01-15 |
wenzelm |
merged
|
file |
diff |
annotate
|
| 2023-01-15 |
wenzelm |
clarified treatment of cite macro name;
|
file |
diff |
annotate
|
| 2023-01-15 |
wenzelm |
updated documentation;
|
file |
diff |
annotate
|
| 2023-01-14 |
wenzelm |
update documentation: prefer control-symbol-cartouche form of "cite" antiquotations;
|
file |
diff |
annotate
|
| 2023-01-13 |
wenzelm |
more "cite" antiquotations;
|
file |
diff |
annotate
|
| 2023-01-12 |
desharna |
added session to mirabelle output directory structure
|
file |
diff |
annotate
|
| 2023-01-06 |
wenzelm |
more command-line options;
|
file |
diff |
annotate
|
| 2023-01-05 |
wenzelm |
updated documentation;
|
file |
diff |
annotate
|
| 2022-12-26 |
desharna |
strengthened and renamed lemmas asym_on_iff_irrefl_on_if_trans and asymp_on_iff_irreflp_on_if_transp
|
file |
diff |
annotate
|
| 2022-12-22 |
desharna |
merged
|
file |
diff |
annotate
|
| 2022-12-20 |
desharna |
used transp_on in assumptions of lemmas Multiset.bex_(least|greatest)_element
|
file |
diff |
annotate
|
| 2022-12-19 |
desharna |
added lemma trans_on_lex_prod[simp]
|
file |
diff |
annotate
|
| 2022-12-19 |
desharna |
strengthened and renamed lemma trans_converse and added lemma transp_on_conversep
|
file |
diff |
annotate
|
| 2022-12-19 |
desharna |
strengthened and renamed trans_reflclI
|
file |
diff |
annotate
|
| 2022-12-19 |
desharna |
strengthened and renamed transp_reflclp
|
file |
diff |
annotate
|
| 2022-12-19 |
desharna |
strengthened and renamed lemmas preorder.transp_(ge|gr|le|less)
|
file |
diff |
annotate
|
| 2022-12-19 |
desharna |
added lemmas trans_on_subset and transp_on_subset
|
file |
diff |
annotate
|
| 2022-12-19 |
desharna |
added lemmas trans_onD and transp_onD
|
file |
diff |
annotate
|
| 2022-12-19 |
desharna |
added lemmas trans_onI and transp_onI
|
file |
diff |
annotate
|
| 2022-12-19 |
desharna |
added lemma transp_on_trans_on_eq[pred_set_conv]
|
file |
diff |
annotate
|
| 2022-12-19 |
desharna |
added predicates trans_on and transp_on and redefined trans and transp to be abbreviations
|
file |
diff |
annotate
|
| 2022-12-22 |
desharna |
merged
|
file |
diff |
annotate
|
| 2022-12-21 |
desharna |
added lemmas irrefl_on_if_asym_on[simp] and irreflp_on_if_asymp_on[simp]
|
file |
diff |
annotate
|
| 2022-12-21 |
wenzelm |
NEWS;
|
file |
diff |
annotate
|
| 2022-12-19 |
desharna |
added lemma refl_lex_prod[simp]
|
file |
diff |
annotate
|
| 2022-12-19 |
desharna |
added lemmas reflI and reflD
|
file |
diff |
annotate
|
| 2022-12-19 |
desharna |
added lemmas asym_on_lex_prod[simp] and asym_lex_prod[simp]
|
file |
diff |
annotate
|
| 2022-12-19 |
desharna |
added lemmas sym_on_lex_prod[simp] and sym_lex_prod[simp]
|
file |
diff |
annotate
|
| 2022-12-19 |
desharna |
added lemmas irrefl_on_lex_prod[simp] and irrefl_lex_prod[simp]
|
file |
diff |
annotate
|
| 2022-12-19 |
desharna |
strengthened and renamed lemmas asym_if_irrefl_and_trans and asymp_if_irreflp_and_transp
|
file |
diff |
annotate
|
| 2022-12-19 |
desharna |
strengthened and renamed lemma antisym_converse and added lemma antisymp_on_conversep
|
file |
diff |
annotate
|
| 2022-12-19 |
desharna |
added lemmas asym_on_converse[simp] and asymp_on_conversep[simp]
|
file |
diff |
annotate
|
| 2022-12-19 |
desharna |
strengthened and renamed lemma sym_converse and added lemma symp_on_conversep
|
file |
diff |
annotate
|
| 2022-12-19 |
desharna |
strengthened and renamed lemmas antisymp_less and antisymp_greater
|
file |
diff |
annotate
|
| 2022-12-19 |
desharna |
strengthened lemmas antisym_on_if_asym_on and antisymp_on_if_asymp_on
|
file |
diff |
annotate
|
| 2022-12-19 |
desharna |
added lemma asymp_on_asym_on_eq[pred_set_conv]
|
file |
diff |
annotate
|
| 2022-12-19 |
desharna |
strengthened and renamed asymp_less and asymp_greater
|
file |
diff |
annotate
|
| 2022-12-19 |
desharna |
added lemmas asym_onI, asymp_onI, asym_onD, and asymp_onD
|
file |
diff |
annotate
|
| 2022-12-18 |
desharna |
added predicates asym_on and asymp_on and redefined asym and asymp to be abbreviations
|
file |
diff |
annotate
|
| 2022-12-16 |
desharna |
strengthened and renamed symp_symclp
|
file |
diff |
annotate
|
| 2022-12-16 |
desharna |
added lemmas sym_on_subset and symp_on_subset
|
file |
diff |
annotate
|
| 2022-12-16 |
desharna |
added lemmas sym_onD and symp_onD
|
file |
diff |
annotate
|
| 2022-12-16 |
desharna |
added lemmas sym_onI and symp_onI
|
file |
diff |
annotate
|
| 2022-12-16 |
desharna |
added lemma symp_on_sym_on_eq[pred_set_conv]
|
file |
diff |
annotate
|
| 2022-12-16 |
desharna |
added predicates sym_on and symp_on and redefined sym and symp to be abbreviations
|
file |
diff |
annotate
|
| 2022-12-15 |
desharna |
added lemmas antisym_on_subset and antisymp_on_subset
|
file |
diff |
annotate
|
| 2022-12-15 |
desharna |
strengthened antisymp_le and antisymp_ge
|
file |
diff |
annotate
|
| 2022-12-15 |
desharna |
added lemmas antisym_onD and antisymp_onD
|
file |
diff |
annotate
|
| 2022-12-15 |
desharna |
added lemmas antisym_onI and antisymp_onI
|
file |
diff |
annotate
|
| 2022-12-15 |
desharna |
added lemma antisymp_reflcp
|
file |
diff |
annotate
|
| 2022-12-15 |
desharna |
added antisymp_on_antisym_on_eq[pred_set_conv]
|
file |
diff |
annotate
|
| 2022-12-15 |
desharna |
added predicates antisym_on and antisymp_on and redefined antisym and antisymp to be abbreviations
|
file |
diff |
annotate
|
| 2022-12-06 |
desharna |
Strengthened multiset lemmas w.r.t. irrefl and irreflp
|
file |
diff |
annotate
|
| 2022-12-06 |
desharna |
NEWS
|
file |
diff |
annotate
|
| 2022-11-24 |
desharna |
added lemmas asym_if_irrefl_and_trans and asymp_if_irreflp_and_transp
|
file |
diff |
annotate
|
| 2022-11-23 |
desharna |
added lemma totalp_on_converse[simp]
|
file |
diff |
annotate
|
| 2022-11-23 |
desharna |
added lemmas irrefl_on_converse[simp] and irreflp_on_converse[simp]
|
file |
diff |
annotate
|
| 2022-11-23 |
desharna |
added type annotations and tuned formatting
|
file |
diff |
annotate
|
| 2022-11-23 |
desharna |
strengthened and renamed irreflp_greater[simp] and irreflp_less[simp]
|
file |
diff |
annotate
|
| 2022-11-23 |
desharna |
added lemmas irrefl_on_subset and irreflp_on_subset
|
file |
diff |
annotate
|
| 2022-11-21 |
desharna |
introduced predicates irrefl_on and irreflp_on, and redefined irrefl and irreflp as abbreviations
|
file |
diff |
annotate
|
| 2022-11-21 |
desharna |
strengthened and renamed lemma reflp_on_equality
|
file |
diff |
annotate
|
| 2022-11-21 |
desharna |
renamed lemmas linorder.totalp_on_(ge|greater|le|less) and preorder.reflp_(ge|le)
|
file |
diff |
annotate
|
| 2022-11-09 |
desharna |
added lemma reflp_on_conversp[simp]
|
file |
diff |
annotate
|
| 2022-11-09 |
desharna |
added lemma transp_reflclp[simp]
|
file |
diff |
annotate
|
| 2022-11-09 |
desharna |
added lemma reflclp_ident_if_reflp[simp]
|
file |
diff |
annotate
|
| 2022-11-09 |
desharna |
added lemma reflp_on_reflclp[simp]
|
file |
diff |
annotate
|
| 2022-11-09 |
desharna |
strengthened lemma reflp_rtranclp and renamed to reflp_on_rtranclp
|
file |
diff |
annotate
|
| 2022-11-06 |
wenzelm |
support for EPTCS style with demo document;
|
file |
diff |
annotate
|
| 2022-11-05 |
wenzelm |
tuned NEWS;
|
file |
diff |
annotate
|
| 2022-11-05 |
wenzelm |
support for Dotnet / Fsharp platform, via dynamically installed Isabelle component;
|
file |
diff |
annotate
|
| 2022-11-04 |
wenzelm |
support for Springer LLNCS with demo document;
|
file |
diff |
annotate
|
| 2022-11-02 |
desharna |
merged
|
file |
diff |
annotate
|
| 2022-10-28 |
desharna |
added lemmas multp_mono_strong and mult_mono_strong
|
file |
diff |
annotate
|
| 2022-10-31 |
wenzelm |
support for FoilTeX with demo document;
|
file |
diff |
annotate
|
| 2022-10-31 |
wenzelm |
support for Easychair style with demo document;
|
file |
diff |
annotate
|
| 2022-10-31 |
wenzelm |
support for Dagstuhl LIPIcs style with demo document;
|
file |
diff |
annotate
|
| 2022-10-21 |
wenzelm |
generic support for XZ and Zstd compression in Isabelle/Scala;
|
file |
diff |
annotate
|
| 2022-10-18 |
wenzelm |
merged
|
file |
diff |
annotate
|
| 2022-10-17 |
wenzelm |
more NEWS;
|
file |
diff |
annotate
|
| 2022-10-15 |
desharna |
added lemma wfP_subset_mset[simp]
|
file |
diff |
annotate
|
| 2022-10-13 |
desharna |
strengthened lemmas preorder.reflp_ge[simp] and preorder.reflp_le[simp]
|
file |
diff |
annotate
|
| 2022-10-13 |
desharna |
added lemmas linorder.totalp_ge[simp], linorder.totalp_greater[simp], linorder.totalp_le[simp], and linorder.totalp_less[simp]
|
file |
diff |
annotate
|
| 2022-10-13 |
desharna |
NEWS
|
file |
diff |
annotate
|
| 2022-10-13 |
desharna |
merged
|
file |
diff |
annotate
|
| 2022-10-13 |
desharna |
fixed NEWS following cee0b9fccf6f
|
file |
diff |
annotate
|
| 2022-10-13 |
desharna |
renamed lemma inj_on_strict_subset to image_strict_mono for symmetry with image_mono and to distinguish from inj_on_subset
|
file |
diff |
annotate
|
| 2022-10-13 |
wenzelm |
merged
|
file |
diff |
annotate
|
| 2022-10-12 |
wenzelm |
support for system option ML_system_apple: emulated x86_64 Poly/ML is sometimes more stable than native ARM64;
|
file |
diff |
annotate
|
| 2022-10-06 |
wenzelm |
more NEWS;
|
file |
diff |
annotate
|
| 2022-10-13 |
desharna |
added lemma fimage_strict_mono
|
file |
diff |
annotate
|
| 2022-10-12 |
desharna |
added lemma wfP_pfsubset
|
file |
diff |
annotate
|
| 2022-10-12 |
desharna |
added lemmas wf_if_convertible_to_wf, wfP_if_convertible_to_wfP, and wfP_if_convertible_to_nat
|
file |
diff |
annotate
|
| 2022-10-11 |
desharna |
added lemmas antisymp_ge[simp], antisymp_greater[simp], antisymp_le[simp], and antisymp_less[simp]
|
file |
diff |
annotate
|
| 2022-10-11 |
desharna |
added lemmas reflp_ge[simp] and reflp_le[simp]
|
file |
diff |
annotate
|
| 2022-10-10 |
desharna |
added lemmas irreflD and irreflpD
|
file |
diff |
annotate
|
| 2022-10-09 |
desharna |
added lemmas antisym_if_asym and antisymp_if_asymp
|
file |
diff |
annotate
|
| 2022-10-09 |
desharna |
strengthened lemma total_on_singleton and added lemma totalp_on_singleton
|
file |
diff |
annotate
|
| 2022-10-02 |
wenzelm |
back to post-release mode -- after fork point;
|
file |
diff |
annotate
|
| 2022-09-30 |
wenzelm |
more explanations on the new order prover (based on 10945fc183cd), without violating strict monotonicity of NEWS wrt. official releases;
|
file |
diff |
annotate
|
| 2022-09-30 |
wenzelm |
restore NEWS, before commit accidents 2aad8698f82f and 10945fc183cd;
|
file |
diff |
annotate
|
| 2022-09-30 |
Lukas Stevens |
added documentation about new order prover
|
file |
diff |
annotate
|
| 2022-09-17 |
wenzelm |
clarified NEWS;
|
file |
diff |
annotate
|
| 2022-09-17 |
wenzelm |
MLton component for x86_64-linux;
|
file |
diff |
annotate
|
| 2022-09-16 |
wenzelm |
more robust: snap version of docker cannot access /tmp;
|
file |
diff |
annotate
|
| 2022-09-14 |
wenzelm |
more items;
|
file |
diff |
annotate
|
| 2022-09-10 |
wenzelm |
more documentation of 'export_classpath' (session ROOT) and 'scala_build_generated_files' (Isar command);
|
file |
diff |
annotate
|
| 2022-09-09 |
wenzelm |
tuning and updates for release;
|
file |
diff |
annotate
|
| 2022-09-09 |
wenzelm |
NEWS;
|
file |
diff |
annotate
|
| 2022-09-08 |
wenzelm |
merged
|
file |
diff |
annotate
|
| 2022-09-08 |
wenzelm |
updated documentation;
|
file |
diff |
annotate
|
| 2022-09-07 |
wenzelm |
clarified message channel for 'print_state' (NB: the command was originally for TTY or Proof General);
|
file |
diff |
annotate
|
| 2022-09-06 |
wenzelm |
option "show_states" for more verbosity of batch-builds;
|
file |
diff |
annotate
|
| 2022-09-07 |
desharna |
merged
|
file |
diff |
annotate
|
| 2022-09-02 |
desharna |
merged
|
file |
diff |
annotate
|
| 2022-06-25 |
desharna |
moved antimono to Fun and redefined it as an abbreviation
|
file |
diff |
annotate
|
| 2022-06-25 |
desharna |
moved mono and strict_mono to Fun and redefined them as abbreviations
|
file |
diff |
annotate
|
| 2022-09-02 |
wenzelm |
more CONTRIBUTORS + NEWS;
|
file |
diff |
annotate
|
| 2022-08-28 |
wenzelm |
more NEWS;
|
file |
diff |
annotate
|
| 2022-08-27 |
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);
|
file |
diff |
annotate
|
| 2022-08-26 |
wenzelm |
merged
|
file |
diff |
annotate
|
| 2022-08-26 |
wenzelm |
support 'chapter_definition' with description for presentation purposes;
|
file |
diff |
annotate
|
| 2022-08-26 |
paulson |
merged
|
file |
diff |
annotate
|
| 2022-08-25 |
paulson |
NEWS about Sum_of_Powers
|
file |
diff |
annotate
|
| 2022-08-25 |
wenzelm |
NEWS;
|
file |
diff |
annotate
|
| 2022-08-25 |
wenzelm |
maintain "uuid" column in session build database, to identity the original build process uniquely;
|
file |
diff |
annotate
|
| 2022-08-24 |
haftmann |
avoid duplicate fact error on global_interpretation of residues
|
file |
diff |
annotate
|
| 2022-08-21 |
wenzelm |
NEWS;
|
file |
diff |
annotate
|
| 2022-08-21 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| 2022-08-21 |
haftmann |
streamlined
|
file |
diff |
annotate
|
| 2022-08-20 |
wenzelm |
merged;
|
file |
diff |
annotate
|
| 2022-08-19 |
wenzelm |
discontinued special support for README.html (which was hardly ever used in the past 2 decades);
|
file |
diff |
annotate
|
| 2022-08-19 |
haftmann |
consolidated attribute name
|
file |
diff |
annotate
|
| 2022-08-17 |
haftmann |
streamlined primitive definitions for integer division
|
file |
diff |
annotate
|
| 2022-08-17 |
blanchet |
tweaked generation of Isar proofs
|
file |
diff |
annotate
|
| 2022-08-12 |
blanchet |
added support for cvc5 (whose interface is almost identical to CVC4)
|
file |
diff |
annotate
|
| 2022-08-11 |
nipkow |
new lemma
|
file |
diff |
annotate
|
| 2022-07-11 |
blanchet |
prefer non-JNI SAT solvers by default in Nitpick
|
file |
diff |
annotate
|
| 2022-07-05 |
wenzelm |
switch to Scala 3;
|
file |
diff |
annotate
|
| 2022-07-05 |
desharna |
added lemmas total_on_trancl and totalp_on_tranclp
|
file |
diff |
annotate
|
| 2022-07-04 |
haftmann |
officical abstract characters for code generation
|
file |
diff |
annotate
|
| 2022-07-01 |
wenzelm |
discontinued Isabelle tools implemented as .scala scripts;
|
file |
diff |
annotate
|
| 2022-06-27 |
traytel |
tuned BNF bounds for function space and bounded sets; NEWS and CONTRIBUTORS
|
file |
diff |
annotate
|
| 2022-06-25 |
wenzelm |
clarified modules;
|
file |
diff |
annotate
|
| 2022-06-24 |
desharna |
merged
|
file |
diff |
annotate
|
| 2022-06-24 |
desharna |
added lemma monotone_on_o
|
file |
diff |
annotate
|
| 2022-06-24 |
desharna |
redefined mono_on and strict_mono_on as an abbreviation of monotone_on
|
file |
diff |
annotate
|
| 2022-06-23 |
desharna |
changed argument order of mono_on and strict_mono_on to uniformize with monotone_on and other predicates
|
file |
diff |
annotate
|
| 2022-06-22 |
haftmann |
Prefer existing horner sum combinator.
|
file |
diff |
annotate
|
| 2022-06-22 |
desharna |
merged
|
file |
diff |
annotate
|
| 2022-06-21 |
desharna |
added lemmas monotone{,_on}_multp_multp_image_mset
|
file |
diff |
annotate
|
| 2022-06-21 |
desharna |
added lemmas monotone_on_empty[simp] and monotone_on_subset
|
file |
diff |
annotate
|
| 2022-06-21 |
desharna |
added predicate monotone_on and redefined monotone to be an abbreviation.
|
file |
diff |
annotate
|
| 2022-06-21 |
wenzelm |
merged
|
file |
diff |
annotate
|
| 2022-06-21 |
wenzelm |
NEWS;
|
file |
diff |
annotate
|
| 2022-06-20 |
desharna |
added lemma map_mono_strict_suffix
|
file |
diff |
annotate
|
| 2022-06-13 |
desharna |
added lemmas image_mset_eq_{image_mset_plus,plus,plus_image_mset}D, and multp_image_mset_image_msetD
|
file |
diff |
annotate
|
| 2022-06-11 |
wenzelm |
promote "isabelle sync" to regular user-space tool, with proper documentation;
|
file |
diff |
annotate
|
| 2022-06-04 |
desharna |
added lemma totalp_on_total_on_eq[pred_set_conv]
|
file |
diff |
annotate
|
| 2022-06-04 |
desharna |
added lemma reflp_on_empty[simp] and totalp_on_empty[simp]
|
file |
diff |
annotate
|
| 2022-06-04 |
desharna |
added lemmas reflp_on_Inf and reflp_on_Sup
|
file |
diff |
annotate
|
| 2022-06-04 |
desharna |
replaced HOL.implies by Pure.imp in reflp_mono for consistency with other lemmas
|
file |
diff |
annotate
|
| 2022-06-04 |
desharna |
added lemmas reflp_on_inf, reflp_on_sup, and reflp_on_mono
|
file |
diff |
annotate
|
| 2022-06-04 |
desharna |
NEWS
|
file |
diff |
annotate
|
| 2022-06-04 |
desharna |
added lemmas reflp_on_subset, totalp_on_subset, and total_on_subset
|
file |
diff |
annotate
|
| 2022-06-04 |
desharna |
introduced predicate reflp_on and redefined reflp to be an abbreviation
|
file |
diff |
annotate
|
| 2022-05-29 |
wenzelm |
tuned whitespace;
|
file |
diff |
annotate
|
| 2022-05-29 |
wenzelm |
merged
|
file |
diff |
annotate
|
| 2022-05-29 |
wenzelm |
more robust: local repository required;
|
file |
diff |
annotate
|
| 2022-05-29 |
wenzelm |
more documentation;
|
file |
diff |
annotate
|
| 2022-05-28 |
desharna |
added lemmas Multiset.bex_{least,greatest}_element
|
file |
diff |
annotate
|
| 2022-05-23 |
desharna |
NEWS
|
file |
diff |
annotate
|
| 2022-05-11 |
wenzelm |
provide Isabelle/Electron test;
|
file |
diff |
annotate
|
| 2022-04-03 |
haftmann |
adjusted printing of type annotations to accomodate Scala 3
|
file |
diff |
annotate
|
| 2022-04-01 |
wenzelm |
tuned spelling;
|
file |
diff |
annotate
|
| 2022-04-01 |
desharna |
added documentation
|
file |
diff |
annotate
|
| 2022-03-29 |
haftmann |
NEWS and CONTRIBUTORS
|
file |
diff |
annotate
|
| 2022-03-25 |
wenzelm |
tuned text, without update of component for now;
|
file |
diff |
annotate
|
| 2022-03-25 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| 2022-03-24 |
wenzelm |
provide pre-built vscodium-1.65.2 for all platforms;
|
file |
diff |
annotate
|
| 2022-03-11 |
desharna |
generated lemma map_ident_strong for BNFs
|
file |
diff |
annotate
|
| 2022-02-18 |
wenzelm |
NEWS;
|
file |
diff |
annotate
|
| 2022-02-17 |
haftmann |
Avoid overaggresive splitting.
|
file |
diff |
annotate
|
| 2022-02-17 |
haftmann |
Avoid overaggresive simplification.
|
file |
diff |
annotate
|
| 2022-02-16 |
desharna |
NEWS
|
file |
diff |
annotate
|
| 2022-02-01 |
blanchet |
tuned NEWS
|
file |
diff |
annotate
|
| 2022-01-31 |
blanchet |
more NEWS
|
file |
diff |
annotate
|
| 2022-01-31 |
blanchet |
updated NEWS
|
file |
diff |
annotate
|
| 2022-01-26 |
blanchet |
treat 'using X by meson' as 'by (meson X)' to avoid loss of polymorphism (cf. metis)
|
file |
diff |
annotate
|
| 2022-01-22 |
desharna |
renamed run_action to run in Mirabelle.action record
|
file |
diff |
annotate
|
| 2022-01-20 |
desharna |
NEWS
|
file |
diff |
annotate
|
| 2022-01-11 |
desharna |
split option "sledgehammer_atp_dest_dir" into "sledgehammer_atp_prob_dest_dir" and "sledgehammer_atp_proof_dest_dir"
|
file |
diff |
annotate
|
| 2021-12-21 |
wenzelm |
support Gradle as alternative to Maven (again);
|
file |
diff |
annotate
|
| 2021-12-19 |
desharna |
NEWS
|
file |
diff |
annotate
|
| 2021-12-06 |
wenzelm |
discontinued old-style {* verbatim *} tokens;
|
file |
diff |
annotate
|
| 2021-11-27 |
desharna |
redefined less_multiset to be based on multp
|
file |
diff |
annotate
|
| 2021-11-27 |
desharna |
added lemma mono_multp
|
file |
diff |
annotate
|
| 2021-11-26 |
desharna |
added Multiset.multp as predicate equivalent of Multiset.mult
|
file |
diff |
annotate
|
| 2021-11-26 |
wenzelm |
merged
|
file |
diff |
annotate
|
| 2021-11-26 |
wenzelm |
NEWS on "isabelle mirabelle";
|
file |
diff |
annotate
|
| 2021-11-26 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| 2021-11-25 |
wenzelm |
clarified default for kodkod_scala;
|
file |
diff |
annotate
|