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 -50 -30 +30 tip

tuned;
3 weeks ago, by wenzelm
explicit "dest" rules: no longer declare [elim_format, elim];
3 weeks ago, by wenzelm
more accurate declarations;
3 weeks ago, by wenzelm
avoid redundant argument (amending af6f55b15749);
3 weeks ago, by wenzelm
tuned;
3 weeks ago, by wenzelm
clarified output;
3 weeks ago, by wenzelm
tuned;
3 weeks ago, by wenzelm
added lemmas
2 weeks ago, by nipkow
A few more lemmas
3 weeks ago, by paulson
A number of basic and unaccountably missing lemmas about complex exponentiation
3 weeks ago, by paulson
Lemmas about integrals and vector-valued functions
3 weeks ago, by paulson
always use proper context when parsing constants
3 weeks ago, by haftmann
tuned
3 weeks ago, by desharna
merged
3 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";
3 weeks ago, by wenzelm
clarified declaration equivalence --- follow original classical.ML, before 8aa1c98b948b;
3 weeks ago, by wenzelm
tuned source structure;
3 weeks ago, by wenzelm
tuned comments: more formal sections;
3 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);
3 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

less more | (0) -30000 -10000 -3000 -1000 -300 -100 -50 -30 +30 tip

isabelle