isabelle: Graph

eliminate code drop: declarations where none needed default tip
31 hours ago, by haftmann
internal setting to identify pointless code drop: declarations
31 hours ago, by haftmann
clarified colors, following d6a14ed060fb;
30 hours ago, by wenzelm
more comments;
31 hours ago, by wenzelm
tuned;
31 hours ago, by wenzelm
tuned;
31 hours ago, by wenzelm
back to more basic defaults, independently on the accidental L&F: e.g. relevant for editor_style=false, and session_graph.pdf;
2 days ago, by wenzelm
proper default colors (amending e840461d5370): e.g. relevant for session_graph.pdf;
2 days ago, by wenzelm
eliminate odd Unicode characters (amending e9f3b94eb6a0, b69e4da2604b, 8f0b2daa7eaa, 8d1e295aab70);
3 days ago, by wenzelm
clarified natural decl_ord vs. slightly odd merge_decl_ord, following the historic status-quo of 53e56e6a67c3, which originally stems from c06d01f75764;
3 days ago, by wenzelm
clarified merge order: accurately reproduce the stable status-quo from 53e56e6a67c3 --- e.g. relevant for smt proof reconstruction in (line 6705 of "$AFP/Modular_arithmetic_LLL_and_HNF_algorithms/HNF_Mod_Det_Soundness.thy") of AFP/f1299d4f896c;
3 days ago, by wenzelm
clarified decl_ord wrt. kind_ord;
3 days ago, by wenzelm
more diagnostic operations;
4 days ago, by wenzelm
more robust treatment of impossible case;
4 days ago, by wenzelm
clarified name and status of auxiliary operation
5 days ago, by haftmann
moved lemma
6 days ago, by nipkow
added lemma
6 days ago, by nipkow
merged
8 days ago, by paulson
Complex analysis lemmas
8 days ago, by paulson
merged
8 days ago, by wenzelm
merged
8 days ago, by wenzelm
more robust, for typical error message prefix/suffix;
9 days ago, by wenzelm
tuned messages;
9 days ago, by wenzelm
NEWS;
9 days ago, by wenzelm
clarified signature: more uniform;
9 days ago, by wenzelm
clarified messages;
9 days ago, by wenzelm
more accurate warning;
9 days ago, by wenzelm
clarified signature;
9 days ago, by wenzelm
tuned (see also 9e7d1c139569);
9 days ago, by wenzelm
tuned;
9 days ago, by wenzelm
clarified signature;
9 days ago, by wenzelm
tuned;
9 days ago, by wenzelm
explicit "dest" rules: no longer declare [elim_format, elim];
9 days ago, by wenzelm
more accurate declarations;
9 days ago, by wenzelm
avoid redundant argument (amending af6f55b15749);
10 days ago, by wenzelm
tuned;
10 days ago, by wenzelm
clarified output;
10 days ago, by wenzelm
tuned;
10 days ago, by wenzelm
added lemmas
8 days ago, by nipkow
A few more lemmas
10 days ago, by paulson
A number of basic and unaccountably missing lemmas about complex exponentiation
10 days ago, by paulson
Lemmas about integrals and vector-valued functions
11 days ago, by paulson
always use proper context when parsing constants
12 days ago, by haftmann
tuned
11 days ago, by desharna
merged
11 days ago, by wenzelm
proper thm ord that conforms to Thm.eq_thm_prop (amending f5fd9b41188a): relevant for declarations in a locale contex with assumptions, e.g. "locale test = assumes True begin declare refl [rule del] end";
12 days ago, by wenzelm
clarified declaration equivalence --- follow original classical.ML, before 8aa1c98b948b;
12 days ago, by wenzelm
tuned source structure;
12 days ago, by wenzelm
tuned comments: more formal sections;
12 days ago, by wenzelm
proper "plain" rule for extra_netpair (amending 8aa1c98b948b): need to avoid flat_rule / Object_Logic.atomize_prems for the sake of "standard" Isar proof, e.g. (line 34 of "$AFP/AWN/Qmsg_Lifting.thy);
12 days ago, by wenzelm
more robust: no failure on bad rule;
12 days ago, by wenzelm
tuned;
12 days ago, by wenzelm
more accurate delete operation via authentic index --- minor performance tuning;
12 days ago, by wenzelm
minor performance tuning;
13 days ago, by wenzelm
clarified signature: do not expose internal data structures;
13 days ago, by wenzelm
clarified signature;
13 days ago, by wenzelm
clarified signature: prefer canonical order (latest declarations first);
13 days ago, by wenzelm
clarified print order: follow original classical.ML, before 8aa1c98b948b;
13 days ago, by wenzelm
maintain collective rule declarations via type Bires.decls, with netpair operations derived from it;
13 days ago, by wenzelm
tuned: order does not matter here;
13 days ago, by wenzelm
clarified modules;
13 days ago, by wenzelm
clarified signature: rule declarations work via "info" as internal rule (which coincides with external rule);
13 days ago, by wenzelm
more accurate "next" counter for each insert operation: subtle change of semantics wrt. Item_Net.length, due to delete operation;
2 weeks ago, by wenzelm
tuned proof;
2 weeks ago, by wenzelm
clarified modules;
2 weeks ago, by wenzelm
redundant: Net.DELETE already handled;
2 weeks ago, by wenzelm
tuned;
2 weeks ago, by wenzelm
clarified signature: more explicit types, notably (thm option) instead of (thm list);
2 weeks ago, by wenzelm
more robust: unique result expected, otherwise index calculations will go wrong;
2 weeks ago, by wenzelm
tuned;
2 weeks ago, by wenzelm
tuned;
2 weeks ago, by wenzelm
clarified signature: anticipate use in src/Provers/classical.ML;
2 weeks ago, by wenzelm
clarified signature;
2 weeks ago, by wenzelm
tuned source structure;
2 weeks ago, by wenzelm
efficient rule declarations in canonical order, for update of netpairs and print operation;
2 weeks ago, by wenzelm
added option `-S` to Mirabelle to specify the subgoal classes to consider
13 days ago, by desharna
moved to more appropriate theory
2 weeks ago, by haftmann
more correct lemma name
2 weeks ago, by haftmann
merged
2 weeks ago, by desharna
added basic support for persistent prover data to Sledgehammer
2 weeks ago, by desharna
merged
2 weeks ago, by wenzelm
tuned comments;
2 weeks ago, by wenzelm
tuned messages;
2 weeks ago, by wenzelm
clarified signature: more explicit type Bires.kind;
2 weeks ago, by wenzelm
tuned;
2 weeks ago, by wenzelm
tuned;
2 weeks ago, by wenzelm
tuned signature;
2 weeks ago, by wenzelm
proper weight, instead of magic number 1000000 (see b3f190995bc9);
2 weeks ago, by wenzelm
just one type Bires.netpair, based on Bires.tag with explicit weight;
2 weeks ago, by wenzelm
misc tuning and clarification;
2 weeks ago, by wenzelm
tuned signature: do not expose private operation;
2 weeks ago, by wenzelm
minor performance tuning;
2 weeks ago, by wenzelm
clarified modules;
2 weeks ago, by wenzelm
clarified signature;
2 weeks ago, by wenzelm
tuned signature: more explicit types;
2 weeks ago, by wenzelm
clarified modules: explicit structure Bires;
2 weeks ago, by wenzelm
minor performance tuning;
3 weeks ago, by wenzelm
Two lemmas and a comment
2 weeks ago, by paulson
removed duplicate lemma; added the notion of the kernel of a function
3 weeks ago, by nipkow
isabelle regenerate_cooper
3 weeks ago, by haftmann
NEWS;
3 weeks ago, by wenzelm
obsolete (see 09904d5ef1f0);
3 weeks ago, by wenzelm
inline errors as "bad" markup;
3 weeks ago, by wenzelm
more robust result of migrate_file: retain full src_path (in contrast to d5d0e36eda16);
3 weeks ago, by wenzelm
clarified signature: more explicit operations;
3 weeks ago, by wenzelm
more robust: avoid crash on session database errors;
3 weeks ago, by wenzelm
tuned signature: more operations;
3 weeks ago, by wenzelm
basic support to reload theory markup from session store;
3 weeks ago, by wenzelm
tuned;
3 weeks ago, by wenzelm
tuned;
3 weeks ago, by wenzelm
tuned;
3 weeks ago, by wenzelm
clarified signature;
3 weeks ago, by wenzelm
eliminate odd workaround from Aug-2012 (see 393a37003851);
3 weeks ago, by wenzelm
tuned;
3 weeks ago, by wenzelm
clarified signature;
3 weeks ago, by wenzelm
tuned signature;
3 weeks ago, by wenzelm
clarified signature: avoid Session with accidental Resources.bootstrap, which is mostly undefined;
3 weeks ago, by wenzelm
clarified signature: prefer private operation (see also 803731b62180);
3 weeks ago, by wenzelm
tuned (see also 5c7652e9bc01);
3 weeks ago, by wenzelm
tuned signature: more generic operations;
3 weeks ago, by wenzelm
clarified signature;
3 weeks ago, by wenzelm
clarified signature: omit pointless object-oriented indirection;
3 weeks ago, by wenzelm
clarified signature;
3 weeks ago, by wenzelm
tuned: avoid overlapping scopes;
3 weeks ago, by wenzelm
tuned;
3 weeks ago, by wenzelm
typo
3 weeks ago, by haftmann
append (rather than prepend) code equations: the order within a theory is maintained in the resulting code
4 weeks ago, by haftmann
scope pending code equations to theories
4 weeks ago, by haftmann
merged
4 weeks ago, by nipkow
tuned
4 weeks ago, by nipkow
enforce rebuild of Isabelle/ML;
4 weeks ago, by wenzelm
proper build_context.store, instead of circular null value (amending 0e36478a1b6a and e891ff63e6db);
4 weeks ago, by wenzelm
merged
4 weeks ago, by wenzelm
more operations (e.g. for testing);
4 weeks ago, by wenzelm
tuned;
4 weeks ago, by wenzelm
tuned signature: more explicit operations;
4 weeks ago, by wenzelm
more accurate ML_Settings from underlying Session;
4 weeks ago, by wenzelm
more accurate ML_Settings from underlying Session;
4 weeks ago, by wenzelm
tuned signature;
4 weeks ago, by wenzelm
clarified signature;
4 weeks ago, by wenzelm
more robust session startup, notably Isabelle/jEdit with session build (amending 0e36478a1b6a);
4 weeks ago, by wenzelm
clarified signature: more accurate ML_Settings;
4 weeks ago, by wenzelm
clarified modules;
4 weeks ago, by wenzelm
clarified signature: avoid duplicate ML_Settings.system;
4 weeks ago, by wenzelm
clarified signature: general Session.open_session_context;
4 weeks ago, by wenzelm
tuned;
4 weeks ago, by wenzelm
tuned;
4 weeks ago, by wenzelm
tuned;
4 weeks ago, by wenzelm
clarified modules;
4 weeks ago, by wenzelm
more uniform options for session build/start (coincides with PIDE.options.value initially);
4 weeks ago, by wenzelm
clarified signature: Session always provides Store (with Rich_Text.Cache);
4 weeks ago, by wenzelm
clarified signature: prefer implicit PIDE.options, which correspond to PIDE.session;
4 weeks ago, by wenzelm
clarified modules;
4 weeks ago, by wenzelm
tuned signature;
4 weeks ago, by wenzelm
clarified signature;
4 weeks ago, by wenzelm
tuned;
4 weeks ago, by wenzelm
clarified signature: more explicit subtypes of Session, with corresponding subtypes of Resources;
4 weeks ago, by wenzelm
re-use cache from Main_Plugin.start;
4 weeks ago, by wenzelm
clarified signature, following c3793899b880;
4 weeks ago, by wenzelm
more robust: assertion holds, because session.finished_theories provides Snapshot from Document.State.end_theory;
4 weeks ago, by wenzelm
clarified signature;
4 weeks ago, by wenzelm
clarified signature;
4 weeks ago, by wenzelm
tuned comments;
4 weeks ago, by wenzelm
tuned;
4 weeks ago, by wenzelm
added lemmas
4 weeks ago, by nipkow
added lemmas
4 weeks ago, by nipkow
treat map_filter similar to list_all, list_ex, list_ex1
5 weeks ago, by haftmann
reinstated intersection of lists as inter_list_set
5 weeks ago, by nipkow
merged
5 weeks ago, by nipkow
defined mset in terms of its list-versin count_list instead of the ugly length of filter.
5 weeks ago, by nipkow
more explicit theorem names for list quantifiers
5 weeks ago, by haftmann
support for explicit ML platform identifier;
5 weeks ago, by wenzelm
more robust;
5 weeks ago, by wenzelm
proper SSH operation (amending 956ecf2c07a0);
5 weeks ago, by wenzelm
more robust;
5 weeks ago, by wenzelm
tuned errors;
5 weeks ago, by wenzelm
merged
5 weeks ago, by wenzelm
tuned message;
5 weeks ago, by wenzelm
more NEWS;
5 weeks ago, by wenzelm
clarified signature;
5 weeks ago, by wenzelm
more flexible ML_Settings in Isabelle/Scala, depending on system options and some default settings;
5 weeks ago, by wenzelm
support dynamic usage_text, after some options have been processed already;
5 weeks ago, by wenzelm
clarified signature: more modular, avoid adhoc mixins;
5 weeks ago, by wenzelm
tuned signature: more operations;
5 weeks ago, by wenzelm
clarified signature: more explicit types;
5 weeks ago, by wenzelm
proper support for old versions before 0e41f26a0250;
5 weeks ago, by wenzelm
tuned whitespace;
5 weeks ago, by wenzelm
proper Java command-line for desktop application (amending a3e7732b0393);
5 weeks ago, by wenzelm
more robust: inspect true ML environment instead of reconstructing it externally;
5 weeks ago, by wenzelm
clarified signature;
5 weeks ago, by wenzelm
discontinue unused parameter (better done as system option);
5 weeks ago, by wenzelm
discontinued ML_IDENTIFIER settings variable;
5 weeks ago, by wenzelm
clarified modules;
5 weeks ago, by wenzelm
tuned;
5 weeks ago, by wenzelm
clarified signature;
5 weeks ago, by wenzelm
removed pointless leftovers
5 weeks ago, by nipkow
more minus_list lemmas (incl code via fold instead of foldr)
5 weeks ago, by nipkow
make canonical homomorphism [simp]
5 weeks ago, by nipkow
the canonical homomorphism should be [simp]
5 weeks ago, by nipkow
merged
5 weeks ago, by nipkow
added minus functions on lists
5 weeks ago, by nipkow
more robust GUI setup via Java, instead of shell script;
5 weeks ago, by wenzelm
merged
6 weeks ago, by wenzelm
clarified modules;
6 weeks ago, by wenzelm
avoid legacy infixes;
6 weeks ago, by wenzelm
discontinue old infixes;
6 weeks ago, by wenzelm
eliminated transitional lemma
6 weeks ago, by haftmann
tuned whitespace
6 weeks ago, by haftmann
reorganized more code-only operations
6 weeks ago, by haftmann
more qualified auxiliary operations
6 weeks ago, by haftmann
Sylvestre's correction to ex_least_nat_le and other tidying
6 weeks ago, by paulson
New lemmas for floor/ceiling/round, plus tidying
6 weeks ago, by paulson
prefer already existing operation to calculate minimum
7 weeks ago, by haftmann
some more lemmas
7 weeks ago, by haftmann
tuned syntax
7 weeks ago, by haftmann
latex error
7 weeks ago, by nipkow
HOL: minor additions regarding linear algebra
7 weeks ago, by Manuel Eberl
HOL-Combinatorics: more lemmas about permutations
7 weeks ago, by Manuel Eberl
merged
7 weeks ago, by wenzelm
tuned;
7 weeks ago, by wenzelm
obsolete (see 22d65e375c01);
7 weeks ago, by wenzelm
more generic parsing of command spans;
7 weeks ago, by wenzelm
tuned;
7 weeks ago, by wenzelm
support for Thy_Info.get_theories_segments, depending on system option "record_theories";
7 weeks ago, by wenzelm
tuned;
7 weeks ago, by wenzelm
another default code_unfold rule
7 weeks ago, by haftmann
generic executable ranges
7 weeks ago, by haftmann
clarified signature;
7 weeks ago, by wenzelm
explicit abort for big lattice operations over non-empty sets
7 weeks ago, by haftmann
prefer explicit operation to make generated code more abstract
7 weeks ago, by haftmann
tuned theory structure
7 weeks ago, by haftmann
qualify can_select auxiliary operations
7 weeks ago, by haftmann
tuned
8 weeks ago, by haftmann
added lemma
8 weeks ago, by haftmann
annotate auxiliary operations explicitly
8 weeks ago, by haftmann
more correct language
8 weeks ago, by haftmann
more modern qualification of auxiliary operations
8 weeks ago, by haftmann
move legacy simplifier interfaces into separate file
2 months ago, by haftmann
added lemmas
2 months ago, by nipkow
tuned
2 months ago, by haftmann
merged
2 months ago, by wenzelm
merged
2 months ago, by wenzelm
update jedit component;
2 months ago, by wenzelm
clarified colors for "dark" theme -- requires to update jedit component;
2 months ago, by wenzelm
suppress other icon themes: always use default "tango" (which includes "idea-icons") -- requires to update jedit component;
2 months ago, by wenzelm
clarified patches: this is hardly modular anymore;
2 months ago, by wenzelm
redundant;
2 months ago, by wenzelm
three lemmas for HOL-Complex_Analysis, HOL-Computational_Algebra
2 months ago, by Manuel Eberl
provide list-valued interface for simp rules
2 months ago, by haftmann
provide modern interface for solvers
2 months ago, by haftmann
provide modern interface for loopers
2 months ago, by haftmann
tuned argument order an internal names
2 months ago, by haftmann
typo
2 months ago, by haftmann
proper NEWS + CONTRIBUTORS;
2 months ago, by wenzelm
tuned: more antiquotations;
2 months ago, by wenzelm
more concise Isabelle/ML;
2 months ago, by wenzelm
reordered signature
2 months ago, by haftmann
prefer Simplifier over bootstrap-only Raw_Simplifier
2 months ago, by haftmann
Simplifier is a superset of Raw_Simplifier
2 months ago, by haftmann
disambiguate function name wrt. structures Simplifier vs. Raw_Simplifier
2 months ago, by haftmann
clarifed name of structure
2 months ago, by haftmann
update jedit component;
2 months ago, by wenzelm
tuned GUI for macOS (see also https://www.formdev.com/flatlaf/macos);
2 months ago, by wenzelm
tuned NEWS;
2 months ago, by wenzelm
more robust Global Options panel: re-init OptionPane after switch, e.g. after change of "lookAndFeel" and re-init of GutterOptionPane, which implicitly depends on com.formdev.flatlaf.FlatLaf.isLafDark() -- requires to update jedit component;
2 months ago, by wenzelm
more scalable icons -- requires to update jedit component;
2 months ago, by wenzelm
proper scalable icon, also for dark mode -- requires to update jedit component;
2 months ago, by wenzelm
clarified default properties -- requires to update jedit component;
2 months ago, by wenzelm
explicit verbose option;
2 months ago, by wenzelm
clarified default properties -- requires to update jedit component;
2 months ago, by wenzelm
dropped unused ML bindings
2 months ago, by haftmann
merged
2 months ago, by wenzelm
clarified tooltip colors;
2 months ago, by wenzelm
more standard color properties, following org.gjt.sp.util.SyntaxUtilities.getColorHexString();
2 months ago, by wenzelm
tuned colors;
2 months ago, by wenzelm
explicit support for dark GUI themes in Isabelle/jEdit;
2 months ago, by wenzelm
simplified structure of patches;
2 months ago, by wenzelm
Added two lemmas; renamed legacy_Complex_simps
2 months ago, by paulson
contributor
2 months ago, by nipkow
added simproc for cont
2 months ago, by nipkow
clarify Sledgehammer instantiations without preplay (dont_preplay option and tactic provers)
2 months ago, by Lukas Bartl
more robust (amending 4ca84abb16ef): Main_Plugin.start() could happen on other thread, e.g. when $JEDIT_SETTINGS/recent.xml refers to "isabelle-export:" URL;
2 months ago, by wenzelm
added lemma
2 months ago, by nipkow
merged
2 months ago, by wenzelm
clarified settings: these are setup defaults, not necessarily the installed version;
2 months ago, by wenzelm
provide "isabelle caddy_setup" and "isabelle caddy";
2 months ago, by wenzelm
update to current go-1.24.3;
2 months ago, by wenzelm
tuned;
2 months ago, by wenzelm
clarified signature and modules;
2 months ago, by wenzelm
tuned comments;
2 months ago, by wenzelm
clarified signature;
2 months ago, by wenzelm
prefer official precise attribute
2 months ago, by haftmann
Kleene's fixpoint thm
2 months ago, by nipkow
merged
2 months ago, by nipkow
Kleene for lfp
2 months ago, by nipkow
A new lemma
2 months ago, by paulson
merged
2 months ago, by paulson
A few more useful lemmas (about topology)
2 months ago, by paulson
more theorems
2 months ago, by haftmann
merged
2 months ago, by paulson
two more lemmas from the AFP
2 months ago, by paulson
new lemma
2 months ago, by haftmann
consolidate input syntax
2 months ago, by haftmann
More type class things
2 months ago, by paulson
executable sorted_list_of_multiset
2 months ago, by haftmann
Tweaking the ordered semiring type classes
2 months ago, by paulson
merged
2 months ago, by paulson
New type classes unboundedx_dense_order, ordered_semiring_1, ordered_semiring_strict and related material from Complex_Bounded_Operators
2 months ago, by paulson
merged
2 months ago, by wenzelm
more robust output: no markup as last resort;
2 months ago, by wenzelm
clarified signature: more scalable output --- avoid adhoc string concatenations after Pretty.string_of;
3 months ago, by wenzelm
clarified signature: more scalable output;
3 months ago, by wenzelm
tuned;
3 months ago, by wenzelm
more scalable: discontinue odd shortcuts from 6b3739fee456, which produce bulky strings internally;
3 months ago, by wenzelm
tuned
2 months ago, by haftmann
preserved facts order in Sledgehammer's linear minimizer
3 months ago, by desharna
merged
3 months ago, by wenzelm
more scalable;
3 months ago, by wenzelm
more scalable;
3 months ago, by wenzelm
more scalable output;
3 months ago, by wenzelm
tuned document text;
3 months ago, by wenzelm
more navigator positions, after BufferUpdate.LOADED and Buffer.CARET_POSITIONED (see also e48b3ddc4810);
3 months ago, by wenzelm
pass "using" facts as parameters to metis in try0
3 months ago, by desharna
clarified signature
3 months ago, by desharna
proper command message for Sledgehammer's proof methods
3 months ago, by desharna
merged
3 months ago, by desharna
tuned metis_instantiate (import types, support unfixed variables)
3 months ago, by Lukas Bartl
merged
3 months ago, by wenzelm
merged
3 months ago, by wenzelm
update NEWS;
3 months ago, by wenzelm
proper painting of menu accelerator in dark mode;
3 months ago, by wenzelm
clarified patches;
3 months ago, by wenzelm
more uniform init_lafs();
3 months ago, by wenzelm
tuned signature, following 1033ed5d3972;
3 months ago, by wenzelm
update jedit component;
3 months ago, by wenzelm
tuned signature -- requires to update jedit component;
3 months ago, by wenzelm
tuned GUI -- requires to update jedit component;
3 months ago, by wenzelm
more accurate GUI painting;
3 months ago, by wenzelm
clarified GUI calculations for icons;
3 months ago, by wenzelm
tuned;
3 months ago, by wenzelm
more FlatLaf operations (following 35d176c50867) -- requires to update jedit component;
3 months ago, by wenzelm
more accurate GUI property (amending 49ca1a40c04a) -- requires to update jedit component;
3 months ago, by wenzelm
more accurate macOS L&F (see also efc58b56a6c7);
3 months ago, by wenzelm
provide FlatMac themes (see also FlatLaf 3.0);
3 months ago, by wenzelm
tuned imports;
3 months ago, by wenzelm
more FlatLaf operations;
3 months ago, by wenzelm
clarified signature;
3 months ago, by wenzelm
updated to jedit-20250417;
3 months ago, by wenzelm
tuned icons -- requires to update jedit component;
3 months ago, by wenzelm
tuned icons, notably for menus -- requires to update jedit component;
3 months ago, by wenzelm
bundle idea-icons-20250415 with jedit -- requires to update jedit component;
3 months ago, by wenzelm
bundle SVG tango icons with jedit -- requires to update jedit component;
3 months ago, by wenzelm
support scaled svg icons directly in GUIUtilities.loadIcon -- requires to update jedit component;
3 months ago, by wenzelm
update idea-icons: prefer scalable SVG;
3 months ago, by wenzelm
support for SVG icons via com.formdev.flatlaf.extras.FlatSVGIcon from flatlaf-extras (which is based on JSVG);
3 months ago, by wenzelm
misc tuning and clarification;
3 months ago, by wenzelm
update to flatlaf-3.6, with native library support on all platforms;
3 months ago, by wenzelm
injectivity results about sin, cos, cis
3 months ago, by Manuel Eberl
a few small lemmas for HOL and HOL-Analysis
3 months ago, by Manuel Eberl
some material on power series and infinite products
3 months ago, by Manuel Eberl
merged
3 months ago, by paulson
merged
3 months ago, by paulson
More tidying and some variable renaming
3 months ago, by paulson
dropped problematic code equation for multisets for RBT code testing
3 months ago, by Manuel Eberl
removed possible problematic dependency in HOL-Library.Multiset
3 months ago, by Manuel Eberl
HOL-Library: multisets of a given size
3 months ago, by Manuel Eberl
some facts about derivatives of products
3 months ago, by Manuel Eberl
more about formal convergence of power series
3 months ago, by Manuel Eberl
removed name clash in some lemmas
3 months ago, by Manuel Eberl
added orphaned theory to HOL-Analysis
3 months ago, by Manuel Eberl
some facts about power series
3 months ago, by Manuel Eberl
moved some lemmas to where they fit better
3 months ago, by Manuel Eberl
more efficient conversions for symbolic representations
3 months ago, by haftmann
notes on bit shift rewrites
3 months ago, by haftmann
explicit case rule
3 months ago, by haftmann
more lemmas
3 months ago, by haftmann
more lemmas
3 months ago, by haftmann
explicit check for computations on word type
3 months ago, by haftmann
more tidying
3 months ago, by paulson
merged
3 months ago, by paulson
tidied more proofs
3 months ago, by paulson
removed duplicate lemmas
3 months ago, by Manuel Eberl
lots of lemmas for HOL, HOL-{Complex_}Analysis, HOL-Number_Theory
3 months ago, by Manuel Eberl
new lemmas for HOL-Complex_Analysis; overhaul of isolated_zeros
3 months ago, by Manuel Eberl
official theory for using bit shift operations for ordinary arithmetic if feasible
3 months ago, by haftmann
corrected operation
3 months ago, by haftmann
tuned whitespace
3 months ago, by haftmann
Simplified old proofs
3 months ago, by paulson
merged
3 months ago, by wenzelm
update to recent MSYS2 / MinGW, which also works via Cygwin;
3 months ago, by wenzelm
tuned
3 months ago, by haftmann
tuned
3 months ago, by haftmann
tuned
3 months ago, by haftmann
tuned
3 months ago, by haftmann
revamped generation of functions
3 months ago, by haftmann
NEWS
3 months ago, by haftmann
typo
3 months ago, by haftmann
tuned
3 months ago, by desharna
merged
3 months ago, by paulson
Tidied some proofs
3 months ago, by paulson
merged
3 months ago, by wenzelm
clarified signature: more uniform;
3 months ago, by wenzelm
tuned;
3 months ago, by wenzelm
more accurate MinGW path conversion: support locations outside of mingw.root;
3 months ago, by wenzelm
tuned messages;
3 months ago, by wenzelm
tuned;
3 months ago, by wenzelm
more uniform directory structure: Windows DLLs are treated like binaries;
3 months ago, by wenzelm
tuned messages;
3 months ago, by wenzelm
more uniform make_polyml_gmp vs. make_polyml;
3 months ago, by wenzelm
clarified options: explicit use of existing GMP library;
3 months ago, by wenzelm
clarified default options: prefer GMP from source;
3 months ago, by wenzelm
Tidied more messy old proofs
3 months ago, by paulson
more tidying and simplifying
3 months ago, by paulson
merged
3 months ago, by paulson
tidying some old proofs
3 months ago, by paulson
Generalised a lemma and added another
3 months ago, by paulson
merged
3 months ago, by wenzelm
more robust;
3 months ago, by wenzelm
more robust;
3 months ago, by wenzelm
clarified GMP build options, notably for Windows;
3 months ago, by wenzelm
more robust access to GMP library that is provided here;
3 months ago, by wenzelm
clarified command-line;
3 months ago, by wenzelm
tuned;
3 months ago, by wenzelm
tuned;
3 months ago, by wenzelm
more uniform verbose mode;
3 months ago, by wenzelm
more explicit build stages;
3 months ago, by wenzelm
tuned;
3 months ago, by wenzelm
more uniform platform_context.execute;
3 months ago, by wenzelm
more robust shell script;
3 months ago, by wenzelm
tuned comments;
3 months ago, by wenzelm
A couple of new lemmas
3 months ago, by paulson
merged
3 months ago, by wenzelm
clarified Windows: always use MinGW version (it is unclear how to build libgmp-10.dll);
3 months ago, by wenzelm
clarified signature: fewer warnings in IntelliJ IDEA;
3 months ago, by wenzelm
tuned: prefer explicit Bash.exports;
3 months ago, by wenzelm
tuned signature;
3 months ago, by wenzelm
clarified signature: more explicit type Platform_Context;
3 months ago, by wenzelm
added option -G to build GMP library from sources;
3 months ago, by wenzelm
Another Eberl lemma plus tidying
3 months ago, by paulson
Another of Manuel's theorems
3 months ago, by paulson
merged
3 months ago, by paulson
More of Manuel's material
3 months ago, by paulson
removed iprover from try0 because its name is clashing with iProver in Sledgehammer
3 months ago, by desharna
expanded Sledgehammer's schedule (loosely inspired by "Hammering without ATPs" evaluation)
3 months ago, by desharna
added try0's schedule to sledgehammer's schedule
3 months ago, by desharna
clarified signature
3 months ago, by desharna
clarified variable names
3 months ago, by haftmann
tuned
3 months ago, by haftmann
use existing implementations of bit operations if nat is implemented by target-language integer
3 months ago, by haftmann
merged
3 months ago, by wenzelm
more comments;
3 months ago, by wenzelm
mandatory option --enable-ho (see also fc5f10691147);
3 months ago, by wenzelm
update to e-3.2, which is actually 3.2.5;
3 months ago, by wenzelm
reflect nested lists in variables names
3 months ago, by haftmann
Simplified lemma (as suggetsed by Stepan Holub)
3 months ago, by nipkow
incorporate target-language integer implementation of bit shifts into Main
3 months ago, by haftmann
represent constants with explicit typargs to avoid false positives for equality approximations like ‹card UNIV === card UNIV›
3 months ago, by haftmann
restored type reconstruction for nbe: remaining type variables must remain schematic for checking
3 months ago, by haftmann
tuned
3 months ago, by haftmann
merged
3 months ago, by wenzelm
NEWS;
3 months ago, by wenzelm
more documentation;
3 months ago, by wenzelm
update jedit component;
3 months ago, by wenzelm
more navigator positions;
3 months ago, by wenzelm
clarified navigator events: avoid excessive 0 positions;
3 months ago, by wenzelm
more robust: make double-sure that get_text does not crash (see on non-existent file);
3 months ago, by wenzelm
more uniform treatment of open buffer vs. loaded file (NB: setCaretPosition includes selectionNone);
3 months ago, by wenzelm
proper hyperlink column (amending 6898054035d6);
3 months ago, by wenzelm
tuned: setCaretPosition already includes selectNone;
3 months ago, by wenzelm
tuned signature;
3 months ago, by wenzelm
clarified history: eliminate pointless var _current;
3 months ago, by wenzelm
clarified target position: line start + offset (or column);
3 months ago, by wenzelm
tuned source structure;
3 months ago, by wenzelm
eliminated patch: imitate jEdit.gotoMarker more directly;
3 months ago, by wenzelm
tuned;
3 months ago, by wenzelm
tuned signature: proper private vars;
3 months ago, by wenzelm
tuned signature;
3 months ago, by wenzelm
unused;
3 months ago, by wenzelm
suppress NavigatorPlugin and its dependencies -- requires to update jedit component;
3 months ago, by wenzelm
prefer search bar (with navigation buttons) over old-fashioned tool bar -- requires to update jedit component;
3 months ago, by wenzelm
add navigation buttons to search bar, depending on property "navigate-toolbar" -- requires to update jedit component;
3 months ago, by wenzelm
remove goto_buffer in favour of uniform goto_file;
3 months ago, by wenzelm
support goto_file / hyperlink_file with offset;
3 months ago, by wenzelm
update jedit component;
3 months ago, by wenzelm
unused (see also 1046a69fabaa);
3 months ago, by wenzelm
prefer generic action names, to be injected into jEdit codebase eventually;
3 months ago, by wenzelm
support for jEdit.openFiles with "+offset:" specification --- requires to update jedit component;
3 months ago, by wenzelm
more accurate navigator position;
3 months ago, by wenzelm
clarified actions and keyboard shortcuts --- requires to update jedit component;
3 months ago, by wenzelm
tuned GUI (see also a01c1f874362) --- requires to update jedit component;
3 months ago, by wenzelm
support for navigation, independently of Navigator plugin;
3 months ago, by wenzelm
misc tuning: more modular message dispatch;
3 months ago, by wenzelm
provide component for https://files.sketis.net/Isabelle_Naproche-20250328
3 months ago, by wenzelm
tuned signature;
4 months ago, by wenzelm
clarified signature;
4 months ago, by wenzelm
tuned (see also 20b261654e33);
4 months ago, by wenzelm
more robust;
4 months ago, by wenzelm
tuned: fewer warnings in IntelliJ IDEA;
4 months ago, by wenzelm
tuned GUI: follow org.gjt.sp.jedit.search.SearchBar;
4 months ago, by wenzelm
merged
3 months ago, by paulson
Inserted more of Manuel Eberl's material
3 months ago, by paulson
merged
3 months ago, by desharna
tuned NEWS
3 months ago, by desharna
added proof method "iprover" to try0
3 months ago, by desharna
added a user-configurable schedule to try0
3 months ago, by desharna
Lemmas from Manuel Eberl's Q_Analogues
3 months ago, by paulson
Added lemma
3 months ago, by nipkow
more on sorting
3 months ago, by haftmann
tuned whitespaces
3 months ago, by desharna
merged
3 months ago, by paulson
Some generalisations (mostly at the level of type classes) by Alexander Pach
3 months ago, by paulson
tuned
3 months ago, by haftmann