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);
9 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;
9 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;
9 days ago, by wenzelm
clarified decl_ord wrt. kind_ord;
10 days ago, by wenzelm
more diagnostic operations;
10 days ago, by wenzelm
more robust treatment of impossible case;
10 days ago, by wenzelm
clarified name and status of auxiliary operation
11 days ago, by haftmann
moved lemma
13 days ago, by nipkow
added lemma
13 days 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;
2 weeks ago, by wenzelm
tuned;
2 weeks ago, by wenzelm
more accurate delete operation via authentic index --- minor performance tuning;
2 weeks ago, by wenzelm
minor performance tuning;
2 weeks ago, by wenzelm
clarified signature: do not expose internal data structures;
2 weeks ago, by wenzelm
clarified signature;
2 weeks ago, by wenzelm
clarified signature: prefer canonical order (latest declarations first);
2 weeks ago, by wenzelm
clarified print order: follow original classical.ML, before 8aa1c98b948b;
2 weeks ago, by wenzelm
maintain collective rule declarations via type Bires.decls, with netpair operations derived from it;
2 weeks ago, by wenzelm
tuned: order does not matter here;
2 weeks ago, by wenzelm
clarified modules;
2 weeks ago, by wenzelm
clarified signature: rule declarations work via "info" as internal rule (which coincides with external rule);
2 weeks 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;
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

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

isabelle