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
+50
+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
20110826, by huffman
NEWS entry for setsum_norm ~> norm_setsum
20110826, by huffman
make HOLProbability respect set/pred distinction
20110826, by huffman
merged
20110826, by wenzelm
use rename_tac to make proof script more robust (with separate set type, 'clarify' yields different variable names)
20100908, by huffman
merged
20110826, by huffman
generalize and simplify proof of continuous_within_sequentially
20110826, by huffman
add lemma sequentially_imp_eventually_within;
20110826, by huffman
replace some continuous_on lemmas with more general versions
20110825, by huffman
remove legacy theorem Lim_inner
20110825, by huffman
arrange everything related to ordered_euclidean_space class together
20110825, by huffman
generalize and shorten proof of basis_orthogonal
20110825, by huffman
remove dot_lsum and dot_rsum in favor of inner_setsum_{left,right}
20110825, by huffman
merged
20110825, by huffman
generalize lemma finite_imp_compact_convex_hull and related lemmas
20110825, by huffman
generalize some lemmas
20110825, by huffman
generalize lemma convex_cone_hull
20110825, by huffman
rename subset_{interior,closure} to {interior,closure}_mono;
20110825, by huffman
simplify many proofs about subspace and span;
20110825, by huffman
remove duplicate simp declaration
20110825, by huffman
simplify definition of 'interior';
20110825, by huffman
add lemma closure_union;
20110824, by huffman
minimize imports
20110824, by huffman
move everything related to 'norm' method into new theory file Norm_Arith.thy
20110824, by huffman
remove unused lemmas dimensionI, dimension_eq
20110824, by huffman
move geometric progression lemmas from Linear_Algebra.thy to Integration.thy where they are used
20110824, by huffman
merge
20110826, by Cezary Kaliszyk
FSet: Explicit proof without mem_def
20110826, by Cezary Kaliszyk
merged
20110826, by nipkow
added lemma
20110826, by nipkow
less
more

(0)
30000
10000
3000
1000
300
100
50
30
+30
+50
+100
+300
+1000
+3000
+10000
tip