isabelle: Graph

Mercurial Mercurial > repos > isabelle / graph

summary | shortlog | changelog | graph | tags | bookmarks | branches | files | gz | help
less more | (0) -30000 -10000 -3000 -1000 -300 -100 -60 tip

eliminate odd Unicode characters (amending e9f3b94eb6a0, b69e4da2604b, 8f0b2daa7eaa, 8d1e295aab70); default tip
7 hours 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;
8 hours 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;
10 hours ago, by wenzelm
clarified decl_ord wrt. kind_ord;
26 hours ago, by wenzelm
more diagnostic operations;
27 hours ago, by wenzelm
more robust treatment of impossible case;
28 hours ago, by wenzelm
clarified name and status of auxiliary operation
2 days ago, by haftmann
moved lemma
4 days ago, by nipkow
added lemma
4 days ago, by nipkow
merged
5 days ago, by paulson
Complex analysis lemmas
5 days ago, by paulson
merged
6 days ago, by wenzelm
merged
6 days ago, by wenzelm
more robust, for typical error message prefix/suffix;
6 days ago, by wenzelm
tuned messages;
6 days ago, by wenzelm
NEWS;
6 days ago, by wenzelm
clarified signature: more uniform;
6 days ago, by wenzelm
clarified messages;
6 days ago, by wenzelm
more accurate warning;
6 days ago, by wenzelm
clarified signature;
6 days ago, by wenzelm
tuned (see also 9e7d1c139569);
6 days ago, by wenzelm
tuned;
6 days ago, by wenzelm
clarified signature;
6 days ago, by wenzelm
tuned;
6 days ago, by wenzelm
explicit "dest" rules: no longer declare [elim_format, elim];
6 days ago, by wenzelm
more accurate declarations;
7 days ago, by wenzelm
avoid redundant argument (amending af6f55b15749);
7 days ago, by wenzelm
tuned;
7 days ago, by wenzelm
clarified output;
7 days ago, by wenzelm
tuned;
7 days ago, by wenzelm
added lemmas
6 days ago, by nipkow
A few more lemmas
7 days ago, by paulson
A number of basic and unaccountably missing lemmas about complex exponentiation
7 days ago, by paulson
Lemmas about integrals and vector-valued functions
8 days ago, by paulson
always use proper context when parsing constants
9 days ago, by haftmann
tuned
8 days ago, by desharna
merged
9 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";
9 days ago, by wenzelm
clarified declaration equivalence --- follow original classical.ML, before 8aa1c98b948b;
9 days ago, by wenzelm
tuned source structure;
10 days ago, by wenzelm
tuned comments: more formal sections;
10 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);
10 days ago, by wenzelm
more robust: no failure on bad rule;
10 days ago, by wenzelm
tuned;
10 days ago, by wenzelm
more accurate delete operation via authentic index --- minor performance tuning;
10 days ago, by wenzelm
minor performance tuning;
10 days ago, by wenzelm
clarified signature: do not expose internal data structures;
10 days ago, by wenzelm
clarified signature;
10 days ago, by wenzelm
clarified signature: prefer canonical order (latest declarations first);
10 days ago, by wenzelm
clarified print order: follow original classical.ML, before 8aa1c98b948b;
10 days ago, by wenzelm
maintain collective rule declarations via type Bires.decls, with netpair operations derived from it;
10 days ago, by wenzelm
tuned: order does not matter here;
10 days ago, by wenzelm
clarified modules;
10 days ago, by wenzelm
clarified signature: rule declarations work via "info" as internal rule (which coincides with external rule);
10 days ago, by wenzelm
more accurate "next" counter for each insert operation: subtle change of semantics wrt. Item_Net.length, due to delete operation;
11 days ago, by wenzelm
tuned proof;
11 days ago, by wenzelm
clarified modules;
11 days ago, by wenzelm
redundant: Net.DELETE already handled;
12 days ago, by wenzelm
tuned;
12 days ago, by wenzelm
clarified signature: more explicit types, notably (thm option) instead of (thm list);
12 days ago, by wenzelm

less more | (0) -30000 -10000 -3000 -1000 -300 -100 -60 tip

isabelle