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
+30000
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.
generalize constant uniformly_continuous_on
20090602, by huffman
generalize more constants
20090602, by huffman
generalize type of bounded
20090602, by huffman
generalize lemma norm_pastecart
20090602, by huffman
generalize lemma norm_triangle_sub
20090602, by huffman
generalize lemma Lim_unique
20090602, by huffman
generalize lemma closed_cball
20090602, by huffman
generalize Lim_transform lemmas
20090602, by huffman
generalize lemma interior_closed_Un_empty_interior
20090602, by huffman
reuse definition of nets from Limits.thy
20090602, by huffman
replace filters with filter bases
20090602, by huffman
generalize type of 'at' to metric_space
20090602, by huffman
redefine nets as filter bases
20090602, by huffman
new lemmas
20090602, by huffman
limits of Pair using filters
20090601, by huffman
Removed usage of reference in reification
20090603, by hoelzl
corrected spacing in reflection
20090602, by hoelzl
switch atsmldeve back to full test on macbroy23
20090603, by kleing
IsabelleProcess: emit status "ready" after initialization and reports;
20090602, by wenzelm
moved restrict_map_insert to theory Map
20090602, by haftmann
merged
20090602, by haftmann
added Landau theory
20090602, by haftmann
added/moved lemmas by Andreas Lochbihler
20090602, by haftmann
added Fin_Fun theory
20090602, by haftmann
tuned code generator test theories
20090602, by haftmann
OCaml builtin intergers are elusive; avoid
20090602, by haftmann
more aggresive bracketing of let expressions
20090602, by haftmann
tuned whitespace
20090602, by haftmann
merged
20090602, by wenzelm
merged
20090602, by wenzelm
merged
20090602, by chaieb
merged
20090602, by chaieb
merged
20090602, by chaieb
Reverses idempotent; radical of E; generalized logarithm;
20090601, by chaieb
made SML/NJ happy;
20090602, by wenzelm
merged
20090602, by wenzelm
use algebra_simps instead of ring_simps
20090602, by hoelzl
merged, resolving conflict in src/Pure/Isar/attrib.ML;
20090602, by wenzelm
Generalized Integral_add
20090602, by hoelzl
Added theorems about distinct & concat, map & replicate and concat & replicate
20090602, by hoelzl
merged
20090602, by berghofe
Fixed broken code dealing with alternative names.
20090602, by berghofe
Enclosed parts of subsection in @{text ...} to make LaTeX happy.
20090602, by berghofe
Added Convex_Euclidean_Space.thy again.
20090602, by berghofe
made SML/NJ happy
20090602, by haftmann
declare Bfun_def [code del]
20090601, by huffman
simp del > code del
20090601, by huffman
limits of inverse using filters
20090601, by huffman
merged
20090601, by huffman
add [code del] declarations
20090601, by huffman
add dependency on Limits.thy
20090601, by huffman
new lemma
20090601, by nipkow
merged
20090531, by huffman
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
20090531, by huffman
more abstract properties of eventually
20090531, by huffman
new lemmas about eventually; rewrite Lim proofs to use more abstract properties of eventually
20090531, by huffman
generalize at function to class perfect_space
20090529, by huffman
generalize topological notions to class metric_space; add class perfect_space
20090529, by huffman
instance ^ :: (metric_space, finite) metric_space
20090529, by huffman
generalize tendsto and related constants to class metric_space
20090529, by huffman
less
more

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