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.
insert now qualified and with authentic syntax
20090604, by haftmann
lemma about List.foldl and Finite_Set.fold
20090604, by haftmann
dropped legacy ML bindings; tuned
20090604, by haftmann
lemmas about basic set operations and Finite_Set.fold
20090604, by haftmann
merged
20090605, by nipkow
new lemma
20090605, by nipkow
merged
20090605, by huffman
fix type of hnorm
20090605, by huffman
define netlimit in terms of eventually
20090604, by huffman
generalize type of 'at' to topological_space; generalize some lemmas
20090604, by huffman
add extra type constraints for dist, norm
20090604, by huffman
generalize norm method to work over class real_normed_vector
20090604, by huffman
example settings for Poly/ML 5.3 (experimental);
20090604, by wenzelm
uniform (short) ids on both sides;
20090604, by wenzelm
merged
20090604, by wenzelm
finite lemmas
20090604, by nipkow
made SML/NJ happy
20090604, by haftmann
merged
20090604, by nipkow
A few finite lemmas
20090604, by nipkow
removed unused location_of;
20090604, by wenzelm
retrieve ML source files;
20090604, by wenzelm
export file_name;
20090604, by wenzelm
more robust treatment of bootstrap source positions;
20090604, by wenzelm
less experimental polyml5.3;
20090604, by wenzelm
just one ROOT.ML without any cd or ".."  simplifies ML environment references to bootstrap sources;
20090604, by wenzelm
exn_message/raised: ML_Compiler.exception_position;
20090604, by wenzelm
eliminated costly registration of tokens;
20090604, by wenzelm
convert explicitly between Position.T/PolyML.location, without costly registration of tokens;
20090604, by wenzelm
added exception_position (dummy);
20090604, by wenzelm
reraise exceptions to preserve original position (ML system specific);
20090604, by wenzelm
tuned signature;
20090604, by wenzelm
export esc;
20090604, by wenzelm
export value;
20090604, by wenzelm
uniform default settings for E, Vampire, SPASS;
20090604, by wenzelm
merged
20090603, by huffman
add classes for t0, t1, and t2 spaces
20090603, by huffman
generalize type of islimpt
20090603, by huffman
more [code del] declarations
20090603, by huffman
generalize some constants and lemmas to class topological_space
20090603, by huffman
replace class open with class topo
20090603, by huffman
open_dist instance for vectors
20090603, by huffman
instance * :: topological_space
20090603, by huffman
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
less
more

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