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.
simplified basic termination proof
20130308, by nipkow
some simp rules for fset
20130308, by traytel
avoid Infinity which confuses JFreeChart histogram;
20130307, by wenzelm
tuned proofs  more structure, less warnings;
20130307, by wenzelm
tuned signature  prefer terminology of Scala and Axiom;
20130307, by wenzelm
better message (typeunsoundnesses are becoming rare, usually the issue is elsewhere, e.g. in the TSTP proof parser)
20130307, by blanchet
avoid using Arith_Data.dest_sum in extendednat simprocs (it treats 'x  y' as 'x +  y', which is not valid for enat)
20130306, by huffman
netlimit is abbreviation for Lim
20130306, by hoelzl
tuned proofs
20130306, by hoelzl
changed has_derivative_intros into a named theorems collection
20130306, by hoelzl
changed continuous_on_intros into a named theorems collection
20130306, by hoelzl
changed continuous_intros into a named theorems collection
20130306, by hoelzl
add tendsto_eq_intros: they add an additional rewriting step at the rhs of >
20130306, by hoelzl
major redesign: order instead of preorder, new definition of intervals as quotients
20130306, by nipkow
added lemma
20130306, by nipkow
extended numerals
20130306, by nipkow
merged
20130305, by wenzelm
merged
20130305, by wenzelm
removed unused Future.flat, while leaving its influence of Future.map (see bcd6b1aa4db5);
20130305, by wenzelm
extended stream library a little more
20130305, by traytel
extended stream library
20130305, by traytel
generalized lemmas in Extended_Real_Limits
20130305, by hoelzl
eventually nhds represented using sequentially
20130305, by hoelzl
generalized compact_Times to topological_space
20130305, by hoelzl
move lemma Inf to usage point
20130305, by hoelzl
tuned proof of Edelstein fixed point theorem (use continuity of dist and attains_sup)
20130305, by hoelzl
tuned proofs (used continuity of infdist, dist and continuous_attains_sup)
20130305, by hoelzl
generalized continuous/compact_attains_inf/sup from real to linorder_topology
20130305, by hoelzl
continuity of pair operations
20130305, by hoelzl
use generate_topology for second countable topologies, does not require intersection stable basis
20130305, by hoelzl
generalized isGlb_unique
20130305, by hoelzl
complete_linorder is also a complete_distrib_lattice
20130305, by hoelzl
move Liminf / Limsup lemmas on complete_lattices to its own file
20130305, by hoelzl
merged
20130305, by nipkow
New theory of infinityextended types; should replace Extended_xyz eventually
20130305, by nipkow
Avoid ML warning about unreferenced identifier.
20130305, by webertj
polymorphic SPASS is also SPASS
20130305, by blanchet
allow more general coercion maps; tuned;
20130305, by traytel
more lemmas about intervals
20130305, by nipkow
merged
20130304, by wenzelm
refined parallel_proofs = 2: fork whole Isar subproofs, not just terminal ones;
20130304, by wenzelm
join all proofs before scheduling present phase (ordered according to weight);
20130304, by wenzelm
more explicit datatype result;
20130304, by wenzelm
split dense into inner_dense_order and no_top/no_bot
20130220, by hoelzl
move auxiliary lemmas from Library/Extended_Reals to HOL image
20130220, by hoelzl
tuned (extend datatype to inline option)
20130304, by traytel
prefer more systematic Future.flat;
20130303, by wenzelm
more uniform Future.map: always internalize failure;
20130303, by wenzelm
uniform treatment of global/local proofs;
20130303, by wenzelm
tuned;
20130303, by wenzelm
clarified Toplevel.element_result wrt. Toplevel.is_ignored;
20130303, by wenzelm
more Thy_Syntax.element operations;
20130303, by wenzelm
coercioninvariant arguments at work
20130301, by traytel
constants with coercioninvariant arguments (possibility to disable/reenable
20130301, by traytel
simplified Proof.future_proof;
20130228, by wenzelm
provide explicit dummy names (cf. dfe469293eb4);
20130228, by wenzelm
discontinued empty name bindings in 'axiomatization';
20130228, by wenzelm
provide common HOLogic.conj_conv and HOLogic.eq_conv;
20130228, by wenzelm
just one HOLogic.Trueprop_conv, with regular exception CTERM;
20130228, by wenzelm
discontinued obsolete 'axioms' command;
20130228, by wenzelm
less
more

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