Mercurial
Mercurial
>
repos
>
isabelle
/ graph
summary
|
shortlog
|
changelog
| graph |
tags
|
bookmarks
|
branches
|
files
|
gz
|
help
less
more
|
(0)
-30000
-10000
-3000
-1000
-300
-100
-15
+15
+100
+300
tip
Find changesets by keywords (author, files, the commit message), revision number or hash, or
revset expression
.
The revision graph only works with JavaScript-enabled browsers.
tuned;
3 months ago, by wenzelm
clarified output;
3 months ago, by wenzelm
tuned;
3 months ago, by wenzelm
added lemmas
3 months ago, by nipkow
A few more lemmas
3 months ago, by paulson
A number of basic and unaccountably missing lemmas about complex exponentiation
3 months ago, by paulson
Lemmas about integrals and vector-valued functions
3 months ago, by paulson
always use proper context when parsing constants
3 months ago, by haftmann
tuned
3 months ago, by desharna
merged
3 months 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 months ago, by wenzelm
clarified declaration equivalence --- follow original classical.ML, before 8aa1c98b948b;
3 months ago, by wenzelm
tuned source structure;
3 months ago, by wenzelm
tuned comments: more formal sections;
3 months 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 months ago, by wenzelm
less
more
|
(0)
-30000
-10000
-3000
-1000
-300
-100
-15
+15
+100
+300
tip