isabelle: Graph

tuned for readability and got small performance improvement default tip
9 hours ago, by desharna
bring some code equations into natural order
26 hours ago, by haftmann
added missing colon
5 days ago, by haftmann
clarified signature;
5 days ago, by wenzelm
clarified signature;
5 days ago, by wenzelm
more direct support for "command_span" markup property "is_begin";
5 days ago, by wenzelm
clarified signature;
5 days ago, by wenzelm
misc tuning and clarification;
5 days ago, by wenzelm
clarified signature;
5 days ago, by wenzelm
clarified code setup
8 days ago, by haftmann
moved / rearranged lemma
8 days ago, by haftmann
eliminate code drop: declarations where none needed
9 days ago, by haftmann
internal setting to identify pointless code drop: declarations
9 days ago, by haftmann
clarified colors, following d6a14ed060fb;
9 days ago, by wenzelm
more comments;
9 days ago, by wenzelm
tuned;
9 days ago, by wenzelm
tuned;
9 days 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;
10 days ago, by wenzelm
proper default colors (amending e840461d5370): e.g. relevant for session_graph.pdf;
10 days ago, by wenzelm
eliminate odd Unicode characters (amending e9f3b94eb6a0, b69e4da2604b, 8f0b2daa7eaa, 8d1e295aab70);
11 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;
11 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;
11 days ago, by wenzelm
clarified decl_ord wrt. kind_ord;
12 days ago, by wenzelm
more diagnostic operations;
12 days ago, by wenzelm
more robust treatment of impossible case;
12 days ago, by wenzelm
clarified name and status of auxiliary operation
13 days ago, by haftmann
moved lemma
2 weeks ago, by nipkow
added lemma
2 weeks ago, by nipkow
merged
2 weeks ago, by paulson
Complex analysis lemmas
2 weeks ago, by paulson
merged
2 weeks ago, by wenzelm
merged
2 weeks ago, by wenzelm
more robust, for typical error message prefix/suffix;
2 weeks ago, by wenzelm
tuned messages;
2 weeks ago, by wenzelm
NEWS;
2 weeks ago, by wenzelm
clarified signature: more uniform;
2 weeks ago, by wenzelm
clarified messages;
2 weeks ago, by wenzelm
more accurate warning;
2 weeks ago, by wenzelm
clarified signature;
2 weeks ago, by wenzelm
tuned (see also 9e7d1c139569);
2 weeks ago, by wenzelm
tuned;
2 weeks ago, by wenzelm
clarified signature;
2 weeks ago, by wenzelm
tuned;
2 weeks ago, by wenzelm
explicit "dest" rules: no longer declare [elim_format, elim];
2 weeks ago, by wenzelm
more accurate declarations;
2 weeks ago, by wenzelm
avoid redundant argument (amending af6f55b15749);
2 weeks ago, by wenzelm
tuned;
2 weeks ago, by wenzelm
clarified output;
2 weeks ago, by wenzelm
tuned;
2 weeks ago, by wenzelm
added lemmas
2 weeks ago, by nipkow
A few more lemmas
2 weeks ago, by paulson
A number of basic and unaccountably missing lemmas about complex exponentiation
2 weeks ago, by paulson
Lemmas about integrals and vector-valued functions
2 weeks ago, by paulson
always use proper context when parsing constants
2 weeks ago, by haftmann
tuned
2 weeks ago, by desharna
merged
2 weeks 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";
2 weeks ago, by wenzelm
clarified declaration equivalence --- follow original classical.ML, before 8aa1c98b948b;
2 weeks ago, by wenzelm
tuned source structure;
2 weeks ago, by wenzelm
tuned comments: more formal sections;
2 weeks 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);
2 weeks ago, by wenzelm
more robust: no failure on bad rule;
3 weeks ago, by wenzelm
tuned;
3 weeks ago, by wenzelm
more accurate delete operation via authentic index --- minor performance tuning;
3 weeks ago, by wenzelm
minor performance tuning;
3 weeks ago, by wenzelm
clarified signature: do not expose internal data structures;
3 weeks ago, by wenzelm
clarified signature;
3 weeks ago, by wenzelm
clarified signature: prefer canonical order (latest declarations first);
3 weeks ago, by wenzelm
clarified print order: follow original classical.ML, before 8aa1c98b948b;
3 weeks ago, by wenzelm
maintain collective rule declarations via type Bires.decls, with netpair operations derived from it;
3 weeks ago, by wenzelm
tuned: order does not matter here;
3 weeks ago, by wenzelm
clarified modules;
3 weeks ago, by wenzelm
clarified signature: rule declarations work via "info" as internal rule (which coincides with external rule);
3 weeks ago, by wenzelm
more accurate "next" counter for each insert operation: subtle change of semantics wrt. Item_Net.length, due to delete operation;
3 weeks ago, by wenzelm
tuned proof;
3 weeks ago, by wenzelm
clarified modules;
3 weeks ago, by wenzelm
redundant: Net.DELETE already handled;
3 weeks ago, by wenzelm
tuned;
3 weeks ago, by wenzelm
clarified signature: more explicit types, notably (thm option) instead of (thm list);
3 weeks ago, by wenzelm
more robust: unique result expected, otherwise index calculations will go wrong;
3 weeks ago, by wenzelm
tuned;
3 weeks ago, by wenzelm
tuned;
3 weeks ago, by wenzelm
clarified signature: anticipate use in src/Provers/classical.ML;
3 weeks ago, by wenzelm
clarified signature;
3 weeks ago, by wenzelm
tuned source structure;
3 weeks ago, by wenzelm
efficient rule declarations in canonical order, for update of netpairs and print operation;
3 weeks ago, by wenzelm
added option `-S` to Mirabelle to specify the subgoal classes to consider
3 weeks ago, by desharna
moved to more appropriate theory
3 weeks ago, by haftmann
more correct lemma name
3 weeks ago, by haftmann
merged
3 weeks ago, by desharna
added basic support for persistent prover data to Sledgehammer
3 weeks ago, by desharna
merged
3 weeks ago, by wenzelm
tuned comments;
3 weeks ago, by wenzelm
tuned messages;
3 weeks ago, by wenzelm
clarified signature: more explicit type Bires.kind;
3 weeks ago, by wenzelm
tuned;
3 weeks ago, by wenzelm
tuned;
3 weeks ago, by wenzelm
tuned signature;
3 weeks ago, by wenzelm
proper weight, instead of magic number 1000000 (see b3f190995bc9);
3 weeks ago, by wenzelm
just one type Bires.netpair, based on Bires.tag with explicit weight;
3 weeks ago, by wenzelm
misc tuning and clarification;
3 weeks ago, by wenzelm
tuned signature: do not expose private operation;
3 weeks ago, by wenzelm
minor performance tuning;
3 weeks ago, by wenzelm
clarified modules;
3 weeks ago, by wenzelm
clarified signature;
3 weeks ago, by wenzelm
tuned signature: more explicit types;
3 weeks ago, by wenzelm
clarified modules: explicit structure Bires;
3 weeks ago, by wenzelm
minor performance tuning;
4 weeks ago, by wenzelm
Two lemmas and a comment
4 weeks ago, by paulson
removed duplicate lemma; added the notion of the kernel of a function
4 weeks ago, by nipkow
isabelle regenerate_cooper
4 weeks ago, by haftmann
NEWS;
4 weeks ago, by wenzelm
obsolete (see 09904d5ef1f0);
4 weeks ago, by wenzelm
inline errors as "bad" markup;
4 weeks ago, by wenzelm
more robust result of migrate_file: retain full src_path (in contrast to d5d0e36eda16);
4 weeks ago, by wenzelm
clarified signature: more explicit operations;
4 weeks ago, by wenzelm
more robust: avoid crash on session database errors;
4 weeks ago, by wenzelm
tuned signature: more operations;
4 weeks ago, by wenzelm
basic support to reload theory markup from session store;
4 weeks ago, by wenzelm
tuned;
4 weeks ago, by wenzelm
tuned;
4 weeks ago, by wenzelm
tuned;
4 weeks ago, by wenzelm
clarified signature;
4 weeks ago, by wenzelm
eliminate odd workaround from Aug-2012 (see 393a37003851);
4 weeks ago, by wenzelm
tuned;
4 weeks ago, by wenzelm
clarified signature;
4 weeks ago, by wenzelm
tuned signature;
5 weeks ago, by wenzelm
clarified signature: avoid Session with accidental Resources.bootstrap, which is mostly undefined;
5 weeks ago, by wenzelm
clarified signature: prefer private operation (see also 803731b62180);
5 weeks ago, by wenzelm
tuned (see also 5c7652e9bc01);
5 weeks ago, by wenzelm
tuned signature: more generic operations;
5 weeks ago, by wenzelm
clarified signature;
5 weeks ago, by wenzelm
clarified signature: omit pointless object-oriented indirection;
5 weeks ago, by wenzelm
clarified signature;
5 weeks ago, by wenzelm
tuned: avoid overlapping scopes;
5 weeks ago, by wenzelm
tuned;
5 weeks ago, by wenzelm
typo
5 weeks ago, by haftmann
append (rather than prepend) code equations: the order within a theory is maintained in the resulting code
5 weeks ago, by haftmann
scope pending code equations to theories
5 weeks ago, by haftmann
merged
5 weeks ago, by nipkow
tuned
5 weeks ago, by nipkow
enforce rebuild of Isabelle/ML;
5 weeks ago, by wenzelm
proper build_context.store, instead of circular null value (amending 0e36478a1b6a and e891ff63e6db);
5 weeks ago, by wenzelm
merged
5 weeks ago, by wenzelm
more operations (e.g. for testing);
5 weeks ago, by wenzelm
tuned;
5 weeks ago, by wenzelm
tuned signature: more explicit operations;
5 weeks ago, by wenzelm
more accurate ML_Settings from underlying Session;
5 weeks ago, by wenzelm
more accurate ML_Settings from underlying Session;
5 weeks ago, by wenzelm
tuned signature;
5 weeks ago, by wenzelm
clarified signature;
5 weeks ago, by wenzelm
more robust session startup, notably Isabelle/jEdit with session build (amending 0e36478a1b6a);
5 weeks ago, by wenzelm
clarified signature: more accurate ML_Settings;
5 weeks ago, by wenzelm
clarified modules;
5 weeks ago, by wenzelm
clarified signature: avoid duplicate ML_Settings.system;
5 weeks ago, by wenzelm
clarified signature: general Session.open_session_context;
5 weeks ago, by wenzelm
tuned;
5 weeks ago, by wenzelm
tuned;
5 weeks ago, by wenzelm
tuned;
5 weeks ago, by wenzelm
clarified modules;
5 weeks ago, by wenzelm
more uniform options for session build/start (coincides with PIDE.options.value initially);
5 weeks ago, by wenzelm
clarified signature: Session always provides Store (with Rich_Text.Cache);
5 weeks ago, by wenzelm
clarified signature: prefer implicit PIDE.options, which correspond to PIDE.session;
5 weeks ago, by wenzelm
clarified modules;
5 weeks ago, by wenzelm
tuned signature;
5 weeks ago, by wenzelm
clarified signature;
5 weeks ago, by wenzelm
tuned;
5 weeks ago, by wenzelm
clarified signature: more explicit subtypes of Session, with corresponding subtypes of Resources;
5 weeks ago, by wenzelm
re-use cache from Main_Plugin.start;
5 weeks ago, by wenzelm
clarified signature, following c3793899b880;
5 weeks ago, by wenzelm
more robust: assertion holds, because session.finished_theories provides Snapshot from Document.State.end_theory;
5 weeks ago, by wenzelm
clarified signature;
5 weeks ago, by wenzelm
clarified signature;
5 weeks ago, by wenzelm
tuned comments;
5 weeks ago, by wenzelm
tuned;
5 weeks ago, by wenzelm
added lemmas
5 weeks ago, by nipkow
added lemmas
5 weeks ago, by nipkow
treat map_filter similar to list_all, list_ex, list_ex1
6 weeks ago, by haftmann
reinstated intersection of lists as inter_list_set
6 weeks ago, by nipkow
merged
6 weeks ago, by nipkow
defined mset in terms of its list-versin count_list instead of the ugly length of filter.
6 weeks ago, by nipkow
more explicit theorem names for list quantifiers
6 weeks ago, by haftmann
support for explicit ML platform identifier;
6 weeks ago, by wenzelm
more robust;
6 weeks ago, by wenzelm
proper SSH operation (amending 956ecf2c07a0);
6 weeks ago, by wenzelm
more robust;
6 weeks ago, by wenzelm
tuned errors;
6 weeks ago, by wenzelm
merged
6 weeks ago, by wenzelm
tuned message;
6 weeks ago, by wenzelm
more NEWS;
6 weeks ago, by wenzelm
clarified signature;
6 weeks ago, by wenzelm
more flexible ML_Settings in Isabelle/Scala, depending on system options and some default settings;
6 weeks ago, by wenzelm
support dynamic usage_text, after some options have been processed already;
6 weeks ago, by wenzelm
clarified signature: more modular, avoid adhoc mixins;
6 weeks ago, by wenzelm
tuned signature: more operations;
6 weeks ago, by wenzelm
clarified signature: more explicit types;
6 weeks ago, by wenzelm
proper support for old versions before 0e41f26a0250;
6 weeks ago, by wenzelm
tuned whitespace;
6 weeks ago, by wenzelm
proper Java command-line for desktop application (amending a3e7732b0393);
6 weeks ago, by wenzelm
more robust: inspect true ML environment instead of reconstructing it externally;
6 weeks ago, by wenzelm
clarified signature;
6 weeks ago, by wenzelm
discontinue unused parameter (better done as system option);
6 weeks ago, by wenzelm
discontinued ML_IDENTIFIER settings variable;
6 weeks ago, by wenzelm
clarified modules;
6 weeks ago, by wenzelm
tuned;
6 weeks ago, by wenzelm
clarified signature;
6 weeks ago, by wenzelm
removed pointless leftovers
6 weeks ago, by nipkow
more minus_list lemmas (incl code via fold instead of foldr)
6 weeks ago, by nipkow
make canonical homomorphism [simp]
6 weeks ago, by nipkow
the canonical homomorphism should be [simp]
7 weeks ago, by nipkow
merged
7 weeks ago, by nipkow
added minus functions on lists
7 weeks ago, by nipkow
more robust GUI setup via Java, instead of shell script;
7 weeks ago, by wenzelm
merged
7 weeks ago, by wenzelm
clarified modules;
7 weeks ago, by wenzelm
avoid legacy infixes;
7 weeks ago, by wenzelm
discontinue old infixes;
7 weeks ago, by wenzelm
eliminated transitional lemma
7 weeks ago, by haftmann
tuned whitespace
7 weeks ago, by haftmann
reorganized more code-only operations
7 weeks ago, by haftmann
more qualified auxiliary operations
7 weeks ago, by haftmann
Sylvestre's correction to ex_least_nat_le and other tidying
8 weeks ago, by paulson
New lemmas for floor/ceiling/round, plus tidying
8 weeks ago, by paulson
prefer already existing operation to calculate minimum
8 weeks ago, by haftmann
some more lemmas
8 weeks ago, by haftmann
tuned syntax
8 weeks ago, by haftmann
latex error
8 weeks ago, by nipkow
HOL: minor additions regarding linear algebra
8 weeks ago, by Manuel Eberl
HOL-Combinatorics: more lemmas about permutations
8 weeks ago, by Manuel Eberl
merged
2 months ago, by wenzelm
tuned;
2 months ago, by wenzelm
obsolete (see 22d65e375c01);
2 months ago, by wenzelm
more generic parsing of command spans;
2 months ago, by wenzelm
tuned;
2 months ago, by wenzelm
support for Thy_Info.get_theories_segments, depending on system option "record_theories";
2 months ago, by wenzelm
tuned;
2 months ago, by wenzelm
another default code_unfold rule
2 months ago, by haftmann
generic executable ranges
2 months ago, by haftmann
clarified signature;
2 months ago, by wenzelm
explicit abort for big lattice operations over non-empty sets
2 months ago, by haftmann