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.
include session description in chapter index;
20130312, by wenzelm
tuned;
20130312, by wenzelm
more accurate theory links;
20130312, by wenzelm
discontinued "isabelle usedir" option r (reset session path);
20130312, by wenzelm
discontinued "isabelle usedir" option P (remote path);
20130311, by wenzelm
support for 'chapter' specifications within session ROOT;
20130311, by wenzelm
added latex markup
20130312, by nipkow
merged
20130312, by kleing
more snippets
20130312, by kleing
added pairs
20130312, by nipkow
extended set comprehension notation with {pttrn : A . P}
20130312, by nipkow
tuned
20130311, by nipkow
more factorisation of Step & Co
20130311, by nipkow
factored out Step
20130310, by nipkow
merged
20130310, by nipkow
stepwise instantiation is more modular
20130310, by nipkow
generalized subclass relation;
20130310, by haftmann
termination proof for narrowing: fewer assumptions
20130310, by nipkow
accomodate encrypted filesystem on linux;
20130309, by wenzelm
tuned;
20130309, by wenzelm
discontinued theory src/HOL/Library/Eval_Witness  assumptions do not longer hold in presence of abstract types
20130309, by haftmann
updated keywords (cf. 84d01fd733cf);
20130308, by wenzelm
proper type inference for default values
20130308, by blanchet
convert mappings to parametric lifting
20130308, by kuncar
setup_lifting doesn't support a type variable as a raw type
20130308, by kuncar
add [relator_mono] and [relator_distr] rules
20130308, by kuncar
simplify Lift_FSet because we have parametricity in Lifting now
20130308, by kuncar
patch Isabelle ditribution to conform to changes regarding the parametricity
20130308, by kuncar
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
20130308, by kuncar
merged
20130308, by nipkow
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
less
more

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