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.
class real_inner derives from open_dist
20090603, by huffman
introduce class topological_space as a superclass of metric_space
20090603, by huffman
Converted reification to use fold_map instead of Library.foldl_map. Use antiquotations.
20090603, by hoelzl
additional debugging
20090603, by immler
include chainths in every provercall
20090603, by immler
split preparing clauses and writing problemfile;
20090603, by immler
merged
20090603, by huffman
merged
20090602, by huffman
instance ^ :: complete_space
20090602, by huffman
instance * :: complete_space; generalize continuity lemmas for fst, snd, Pair
20090602, by huffman
generalize type of constant lim
20090602, by huffman
class complete_space
20090602, by huffman
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
less
more

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