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
+60
+100
+300
+1000
+3000
+10000
tip
Find changesets by keywords (author, files, the commit message), revision number or hash, or
revset expression
.
The revision graph only works with JavaScriptenabled browsers.
merged
20150702, by wenzelm
more CONTRIBUTORS;
20150702, by wenzelm
documentation for 'subgoal' command;
20150702, by wenzelm
clarified module;
20150702, by wenzelm
allow to specify suffix of goal parameters;
20150702, by wenzelm
subgoal parameters are internal by default and named by user;
20150702, by wenzelm
split multigoals as usual (outermost Pure.conjunction only);
20150701, by wenzelm
clarified prems: full subgoal is imported in any case, to avoid remaining schematic variables;
20150701, by wenzelm
proper state after qed;
20150701, by wenzelm
clarified keyword categories;
20150701, by wenzelm
support for subgoal focus command;
20150701, by wenzelm
tuned;
20150701, by wenzelm
taylor series with has_integral and integrable_on
20150701, by immler
merged
20150630, by wenzelm
no arguments for "standard" (or old "default") methods;
20150630, by wenzelm
renamed "default" to "standard", to make semantically clear what it is;
20150630, by wenzelm
tuned;
20150630, by wenzelm
Merge
20150630, by paulson
Useful lemmas. The theorem concerning swapping the variables in a double integral.
20150630, by paulson
generalized inf and sup_continuous; added intro rules
20150630, by hoelzl
fix texoutput for rel_mset
20150630, by hoelzl
removed chained facts from preplaying  and careful about extra chained facts when removing 'proof ' and 'qed' from oneline Isar proofs
20150629, by blanchet
clarified map_node: operate precisely on goal context and goal info (see also 2b8342b0d98c);
20150629, by wenzelm
improved scheduling for urgent tasks, using farm of replacement threads (may lead to factor 2 overloading, but CPUs are usually hyperthreaded);
20150629, by wenzelm
clarified static phase;
20150629, by wenzelm
tuned proofs;
20150629, by wenzelm
more symbols;
20150629, by wenzelm
more symbols;
20150629, by wenzelm
corrected typo
20150629, by nipkow
tuned src/HOL/ex/Ballot
20150616, by hoelzl
add examples from Freek's top 100 theorems (thms 30, 73, 77)
20150612, by bulwahn
generalized geometric distribution
20150617, by hoelzl
added lemma
20150628, by nipkow
simplified termination criterion for euclidean algorithm (again)
20150627, by haftmann
tuned proof
20150627, by haftmann
rings follow immediately their corresponding semirings
20150627, by haftmann
tuned code setup
20150627, by haftmann
algebraic specification for set gcd
20150627, by haftmann
premises in 'show' are treated like 'assume';
20150627, by wenzelm
adapted to a9b71c82647b;
20150626, by wenzelm
merged
20150626, by wenzelm
isabelle update_cartouches;
20150626, by wenzelm
more symbols;
20150626, by wenzelm
tuned proofs;
20150626, by wenzelm
do not expose goal parameters;
20150626, by wenzelm
more symbols;
20150626, by wenzelm
more symbols;
20150626, by wenzelm
proper spacing, as for other syntax for these symbols;
20150626, by wenzelm
tuned whitespace;
20150626, by wenzelm
updated SystemOnTPTP URL
20150626, by blanchet
tuned proofs;
20150626, by wenzelm
merged
20150625, by wenzelm
implicit goal cases are legacy;
20150625, by wenzelm
tuned proofs;
20150625, by wenzelm
more heap  hoping for more stability of HOLProofs;
20150625, by wenzelm
added method "goals" for proper subgoal cases;
20150625, by wenzelm
tuned signature;
20150625, by wenzelm
tuned signature;
20150625, by wenzelm
tuned;
20150625, by wenzelm
tuned;
20150625, by wenzelm
less
more

(0)
30000
10000
3000
1000
300
100
60
+60
+100
+300
+1000
+3000
+10000
tip