isabelle: Graph

Simplified old proofs
5 months ago, by paulson
merged
5 months ago, by wenzelm
update to recent MSYS2 / MinGW, which also works via Cygwin;
5 months ago, by wenzelm
tuned
5 months ago, by haftmann
tuned
5 months ago, by haftmann
tuned
5 months ago, by haftmann
tuned
5 months ago, by haftmann
revamped generation of functions
5 months ago, by haftmann
NEWS
5 months ago, by haftmann
typo
5 months ago, by haftmann
tuned
5 months ago, by desharna
merged
5 months ago, by paulson
Tidied some proofs
5 months ago, by paulson
merged
5 months ago, by wenzelm
clarified signature: more uniform;
5 months ago, by wenzelm
tuned;
5 months ago, by wenzelm
more accurate MinGW path conversion: support locations outside of mingw.root;
5 months ago, by wenzelm
tuned messages;
5 months ago, by wenzelm
tuned;
5 months ago, by wenzelm
more uniform directory structure: Windows DLLs are treated like binaries;
5 months ago, by wenzelm
tuned messages;
5 months ago, by wenzelm
more uniform make_polyml_gmp vs. make_polyml;
5 months ago, by wenzelm
clarified options: explicit use of existing GMP library;
5 months ago, by wenzelm
clarified default options: prefer GMP from source;
5 months ago, by wenzelm
Tidied more messy old proofs
5 months ago, by paulson
more tidying and simplifying
5 months ago, by paulson
merged
5 months ago, by paulson
tidying some old proofs
5 months ago, by paulson
Generalised a lemma and added another
5 months ago, by paulson
merged
5 months ago, by wenzelm
more robust;
5 months ago, by wenzelm
more robust;
5 months ago, by wenzelm
clarified GMP build options, notably for Windows;
5 months ago, by wenzelm
more robust access to GMP library that is provided here;
5 months ago, by wenzelm
clarified command-line;
5 months ago, by wenzelm
tuned;
5 months ago, by wenzelm
tuned;
5 months ago, by wenzelm
more uniform verbose mode;
5 months ago, by wenzelm
more explicit build stages;
5 months ago, by wenzelm
tuned;
5 months ago, by wenzelm
more uniform platform_context.execute;
5 months ago, by wenzelm
more robust shell script;
5 months ago, by wenzelm
tuned comments;
5 months ago, by wenzelm
A couple of new lemmas
5 months ago, by paulson
merged
5 months ago, by wenzelm
clarified Windows: always use MinGW version (it is unclear how to build libgmp-10.dll);
5 months ago, by wenzelm
clarified signature: fewer warnings in IntelliJ IDEA;
5 months ago, by wenzelm
tuned: prefer explicit Bash.exports;
5 months ago, by wenzelm
tuned signature;
5 months ago, by wenzelm
clarified signature: more explicit type Platform_Context;
5 months ago, by wenzelm
added option -G to build GMP library from sources;
5 months ago, by wenzelm
Another Eberl lemma plus tidying
5 months ago, by paulson
Another of Manuel's theorems
5 months ago, by paulson
merged
5 months ago, by paulson
More of Manuel's material
5 months ago, by paulson
removed iprover from try0 because its name is clashing with iProver in Sledgehammer
5 months ago, by desharna
expanded Sledgehammer's schedule (loosely inspired by "Hammering without ATPs" evaluation)
5 months ago, by desharna
added try0's schedule to sledgehammer's schedule
5 months ago, by desharna
clarified signature
5 months ago, by desharna
clarified variable names
5 months ago, by haftmann
tuned
5 months ago, by haftmann
use existing implementations of bit operations if nat is implemented by target-language integer
5 months ago, by haftmann
merged
5 months ago, by wenzelm
more comments;
5 months ago, by wenzelm
mandatory option --enable-ho (see also fc5f10691147);
5 months ago, by wenzelm
update to e-3.2, which is actually 3.2.5;
5 months ago, by wenzelm
reflect nested lists in variables names
5 months ago, by haftmann
Simplified lemma (as suggetsed by Stepan Holub)
5 months ago, by nipkow
incorporate target-language integer implementation of bit shifts into Main
5 months ago, by haftmann
represent constants with explicit typargs to avoid false positives for equality approximations like ‹card UNIV === card UNIV›
5 months ago, by haftmann
restored type reconstruction for nbe: remaining type variables must remain schematic for checking
5 months ago, by haftmann
tuned
5 months ago, by haftmann
merged
5 months ago, by wenzelm
NEWS;
5 months ago, by wenzelm
more documentation;
5 months ago, by wenzelm
update jedit component;
5 months ago, by wenzelm
more navigator positions;
6 months ago, by wenzelm
clarified navigator events: avoid excessive 0 positions;
6 months ago, by wenzelm
more robust: make double-sure that get_text does not crash (see on non-existent file);
6 months ago, by wenzelm
more uniform treatment of open buffer vs. loaded file (NB: setCaretPosition includes selectionNone);
6 months ago, by wenzelm
proper hyperlink column (amending 6898054035d6);
6 months ago, by wenzelm
tuned: setCaretPosition already includes selectNone;
6 months ago, by wenzelm
tuned signature;
6 months ago, by wenzelm
clarified history: eliminate pointless var _current;
6 months ago, by wenzelm
clarified target position: line start + offset (or column);
6 months ago, by wenzelm
tuned source structure;
6 months ago, by wenzelm
eliminated patch: imitate jEdit.gotoMarker more directly;
6 months ago, by wenzelm
tuned;
6 months ago, by wenzelm
tuned signature: proper private vars;
6 months ago, by wenzelm
tuned signature;
6 months ago, by wenzelm
unused;
6 months ago, by wenzelm
suppress NavigatorPlugin and its dependencies -- requires to update jedit component;
6 months ago, by wenzelm
prefer search bar (with navigation buttons) over old-fashioned tool bar -- requires to update jedit component;
6 months ago, by wenzelm
add navigation buttons to search bar, depending on property "navigate-toolbar" -- requires to update jedit component;
6 months ago, by wenzelm
remove goto_buffer in favour of uniform goto_file;
6 months ago, by wenzelm
support goto_file / hyperlink_file with offset;
6 months ago, by wenzelm
update jedit component;
6 months ago, by wenzelm
unused (see also 1046a69fabaa);
6 months ago, by wenzelm
prefer generic action names, to be injected into jEdit codebase eventually;
6 months ago, by wenzelm
support for jEdit.openFiles with "+offset:" specification --- requires to update jedit component;
6 months ago, by wenzelm
more accurate navigator position;
6 months ago, by wenzelm
clarified actions and keyboard shortcuts --- requires to update jedit component;
6 months ago, by wenzelm
tuned GUI (see also a01c1f874362) --- requires to update jedit component;
6 months ago, by wenzelm
support for navigation, independently of Navigator plugin;
6 months ago, by wenzelm
misc tuning: more modular message dispatch;
6 months ago, by wenzelm
provide component for https://files.sketis.net/Isabelle_Naproche-20250328
6 months ago, by wenzelm
tuned signature;
6 months ago, by wenzelm
clarified signature;
6 months ago, by wenzelm
tuned (see also 20b261654e33);
6 months ago, by wenzelm
more robust;
6 months ago, by wenzelm
tuned: fewer warnings in IntelliJ IDEA;
6 months ago, by wenzelm
tuned GUI: follow org.gjt.sp.jedit.search.SearchBar;
6 months ago, by wenzelm
merged
6 months ago, by paulson
Inserted more of Manuel Eberl's material
6 months ago, by paulson
merged
6 months ago, by desharna
tuned NEWS
6 months ago, by desharna
added proof method "iprover" to try0
6 months ago, by desharna
added a user-configurable schedule to try0
6 months ago, by desharna
Lemmas from Manuel Eberl's Q_Analogues
6 months ago, by paulson
Added lemma
6 months ago, by nipkow
more on sorting
6 months ago, by haftmann
tuned whitespaces
6 months ago, by desharna
merged
6 months ago, by paulson
Some generalisations (mostly at the level of type classes) by Alexander Pach
6 months ago, by paulson
tuned
6 months ago, by haftmann
tuned
6 months ago, by haftmann
tuned
6 months ago, by desharna
tuned
6 months ago, by desharna
tuned signature
6 months ago, by desharna
garbage collection
6 months ago, by blanchet
removed old Vampire configuration from Sledgehammer
6 months ago, by desharna
removed old E configuration from Sledgehammer
6 months ago, by desharna
removed unused function
6 months ago, by desharna
tuned namespace organisation
6 months ago, by haftmann
optional external files as code modules
6 months ago, by haftmann
proper markup for target language code
6 months ago, by haftmann
tuned
6 months ago, by haftmann
tuned
6 months ago, by haftmann
tuned
6 months ago, by haftmann
tuned
6 months ago, by haftmann
spelling
6 months ago, by haftmann
tuned
6 months ago, by desharna
removed debug commands
6 months ago, by desharna
merged
6 months ago, by desharna
refactored tactic-based provers in sledgehammer to use Try0 module
6 months ago, by desharna
tuned stringification of proof method in try0
6 months ago, by desharna
simplified implementation of the_signed_int
6 months ago, by haftmann
tuned
6 months ago, by desharna
merged
6 months ago, by desharna
tuned signature
6 months ago, by desharna
tuned and moved configuration of auto_try0 to theory HOL
6 months ago, by desharna
removed unused function
6 months ago, by desharna
tuned signature
6 months ago, by desharna
moved try0's HOL-specific stuff into own theory
6 months ago, by desharna
moved HOL-specific code out of ML file for generic try0
6 months ago, by desharna
tuned signature
6 months ago, by desharna
tuned
6 months ago, by desharna
refactored try0's internals
6 months ago, by desharna
tuned naming
6 months ago, by desharna
merged
6 months ago, by paulson
Manuel's material on infinite products
6 months ago, by paulson
start jobs even if repository is unreachable, e.g. due to high load;
6 months ago, by Fabian Huch
More from Theta_Functions_Library
6 months ago, by paulson
merged
6 months ago, by paulson
More migration from Theta_Functions_Library
6 months ago, by paulson
added type annotations
6 months ago, by desharna
tuned
6 months ago, by desharna
tuned to avoid list traversal and memory allocation
6 months ago, by desharna
tuned to avoid list traversal and memory allocation
6 months ago, by desharna
tuned to avoid list traversal and memory allocation
6 months ago, by desharna
moved command try0 into its own new theory
6 months ago, by desharna
renamed lemmas
6 months ago, by desharna
merged
6 months ago, by nipkow
weakened hypothesis (suggested by Moritz Roos)
6 months ago, by nipkow
tuned variable names such that A \<subseteq> B
6 months ago, by desharna
New material by Manuel Eberl
6 months ago, by paulson
moved lemmas around
6 months ago, by desharna
added lemmas asymp_on_mono_strong and asymp_on_mono[mono]
6 months ago, by desharna
added lemmas irreflp_on_mono_strong and irreflp_on_mono[mono]
6 months ago, by desharna
tuned variable names
6 months ago, by desharna
tuned proof
6 months ago, by desharna
moved lemmas around
6 months ago, by desharna
removed reflp_mono (use reflp_on_mono_strong instead)
6 months ago, by desharna
added lemma reflp_on_mono[mono]
6 months ago, by desharna
strengthened reflp_on_mono and renamed to reflp_on_mono_strong
6 months ago, by desharna
added lemmas antisymp_on_mono_stronger, antisymp_on_mono_strong, antisymp_on_mono[mono]
6 months ago, by desharna
moved lemmas around
6 months ago, by desharna
proper lemma name
6 months ago, by desharna
added lemmas left_unique_mono_strong, left_unique_mono[mono], right_unique_mono_strong, right_unique_mono[mono]
6 months ago, by desharna
merged
6 months ago, by paulson
Function space instead of image closure
6 months ago, by paulson
remove junk (amending 0811cfce1f5b);
6 months ago, by wenzelm
support for "isabelle jedit -o OPTION";
6 months ago, by wenzelm
discontinue macOS 11 Big Sur;
6 months ago, by wenzelm
reactivate test after upgrade from macOS 11 to 12, with refresh of Xcode + homebrew;
6 months ago, by wenzelm
clarified signature: more explicit type Sessions.Conditions;
6 months ago, by wenzelm
more uniform Proof_Display.print_results for theory and proof output --- avoid loss of information seen in src/Doc/JEdit/document/output-and-state.png (the first bad changeset is f8c412a45af8, see also 53b59fa42696);
6 months ago, by wenzelm
support for writeln_urgent, which is shown in Output before state messages (reminiscent of old Output.urgent_message before 521cea5fa777);
6 months ago, by wenzelm
merged
6 months ago, by desharna
tuned proof
6 months ago, by desharna
added lemma trans_on_diff_Id
6 months ago, by desharna
proper deletion: use facet fields that are not tokenized;
6 months ago, by Fabian Huch
merged
6 months ago, by paulson
New theorems, mostly from the number theory project
6 months ago, by paulson
ZGC of Java 21 is enabled by default: now possible, because Windows Server 2012 (vmnipkow9) has been discontinued;
6 months ago, by wenzelm
tidied old proofs
6 months ago, by paulson
merged
6 months ago, by paulson
tidying old proofs
6 months ago, by paulson
merged
6 months ago, by wenzelm
SSH connections allow zsh as well: this happens to work with the existing Bash.char / Bach.string operations;
6 months ago, by wenzelm
merged
6 months ago, by paulson
Tidied old proofs
6 months ago, by paulson
mini1 is not active due to upgrade;
6 months ago, by wenzelm
fixed missing from a0693649e9c6
6 months ago, by desharna
removed lemma wf_empty (use wf_on_bot instead)
6 months ago, by desharna
added lemmas wf_on_bot[simp] and wfp_on_bot[simp]
6 months ago, by desharna
added lemmas, refl_on_top[simp], reflp_on_top[simp], sym_on_top[simp], symp_on_top[simp], trans_on_top[simp], transp_on_top[simp], total_on_top[simp], totalp_on_top[simp]
6 months ago, by desharna
merged
6 months ago, by desharna
removed lemmas antisym_empty[simp], antisym_bot[simp], trans_empty[simp]
6 months ago, by desharna
added lemmas antisym_on_bot[simp], asym_on_bot[simp], irrefl_on_bot[simp], sym_on_bot[simp], trans_on_bot[simp]
6 months ago, by desharna
merged
6 months ago, by paulson
Tidied up a few messy proofs
6 months ago, by paulson
merged
6 months ago, by paulson
Tidying of old proofs
6 months ago, by paulson
more lemmas
6 months ago, by haftmann
removed theory HOL-Library.Divides (finally)
6 months ago, by haftmann
added lemmas, antisymp_on_bot[simp], asymp_on_bot[simp], irreflp_on_bot[simp], left_unique_bot[simp], symp_on_bot[simp], transp_on_bot[simp]
6 months ago, by desharna
moved left_unique_conversep[simp] and right_unique_conversep[simp] to HOL.Relation
6 months ago, by desharna
added lemmas totalp_on_mono[mono], totalp_on_mono_strong, totalp_on_mono_stronger, totalp_on_mono_stronger_alt
6 months ago, by desharna
removed lemmas left_unique_iff and right_unique_iff
6 months ago, by desharna
added lemma left_unique_iff_Uniq
6 months ago, by desharna
Moved predicate left_unique from HOL.Transfer to HOL.Relation
6 months ago, by desharna
merged
6 months ago, by desharna
proper theory name in NEWS
6 months ago, by desharna
removed single_valuedp (use right_unique instead)
6 months ago, by desharna
merged
6 months ago, by wenzelm
more robust windows_app: bundle current 7z 24.09, but downgrade its output to 16.02, in order to work with old/unmaintained 7zsd_extra_171_3901.7z --- consequently, "Admin/build_release -p windows" works uniformly on Ubuntu 22.04 and 24.04;
6 months ago, by wenzelm
support for .tar.xz archives;
6 months ago, by wenzelm
moved predicate right_unique to theory Relation
6 months ago, by desharna
added lemma single_valuedp_eq_right_unique
6 months ago, by desharna