Mercurial
Mercurial
>
repos
>
isabelle
/ graph
summary

shortlog

changelog
 graph 
tags

bookmarks

branches

files

gz

help
less
more

(0)
30000
10000
3000
1000
120
+120
+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.
merged
20090609, by wenzelm
merged
20090609, by huffman
instance heine_borel < complete_space; generalize many lemmas to class heine_borel
20090609, by huffman
new class heine_borel for lemma bounded_closed_imp_compact; instances for real, ^
20090609, by huffman
generalize compact/closure lemmas
20090608, by huffman
add lemma complete_imp_closed
20090608, by huffman
generalize constant 'bounded' to class metric_space
20090608, by huffman
generalize lemmas compact_imp_bounded, compact_imp_closed
20090608, by huffman
generalize more lemmas
20090608, by huffman
generalize constant 'indirection'
20090608, by huffman
lemmas about linear, bilinear
20090608, by huffman
generalize constant 'complete'
20090608, by huffman
generalize lemmas eventually_within_interior, lim_within_interior
20090608, by huffman
generalize more lemmas
20090608, by huffman
generalize some lemmas
20090608, by huffman
avoiding duplicate definitions of executable functions
20090609, by bulwahn
tuned;
20090609, by wenzelm
more native Scala style;
20090609, by wenzelm
tuned;
20090609, by wenzelm
simplified IsabelleSystem.platform_path for cygwin;
20090609, by wenzelm
merged
20090609, by wenzelm
removed duplicate lemmas
20090609, by himmelma
removed general graph functions in the predicate compiler
20090609, by bulwahn
added graph builders
20090609, by bulwahn
removed debug messages
20090609, by bulwahn
refactoring the predicate compiler
20090609, by bulwahn
merged
20090609, by chaieb
Tuned sos tactic to reject non SOS goals
20090609, by chaieb
tuned
20090609, by boehmes
fast_lin_arith uses proper multiplication instead of unfolding to additions
20090608, by boehmes
more lemmas
20090608, by nipkow
Better approximation of cos around pi.
20090608, by hoelzl
merged
20090608, by huffman
merged
20090607, by huffman
new lemma
20090608, by nipkow
merged
20090608, by haftmann
merged
20090608, by haftmann
proper deresolving of class relations and class parameters in SML
20090608, by haftmann
New lemma
20090608, by nipkow
eliminated hardwired Cygwin setup;
20090608, by wenzelm
Accessing the Cygwin installation.
20090608, by wenzelm
static IsabelleSystem.charset;
20090607, by wenzelm
isabelle getenv: option d;
20090607, by wenzelm
no parallel make jobs on macbroy23, which is the machine where SML/XL is tested  attempt to consume less resources;
20090606, by wenzelm
updated version;
20090606, by wenzelm
fix type of open
20090607, by huffman
new setL2 lemmas; instance ^ :: (topological_space, finite) topological_space
20090607, by huffman
replace 'topo' with 'open'; add extra type constraint for 'open'
20090607, by huffman
generalize tendsto lemmas for products
20090607, by huffman
move definitions of open, closed to RealVector.thy
20090607, by huffman
lemmas islimptI, islimptE; generalize open_inter_closure_subset
20090606, by huffman
generalize tendsto to class topological_space
20090606, by huffman
put syntax for tendsto in Limits.thy; rename variables
20090605, by huffman
constant "chars" of all characters
20090608, by haftmann
added infrastructure for definitorial construction of generators for datatypes
20090608, by haftmann
constant "chars" of all characters
20090608, by haftmann
added generator for char and trivial generator for String.literal
20090608, by haftmann
using constant "chars"
20090608, by haftmann
method linarith
20090608, by haftmann
reraise exceptions to preserve position information;
20090606, by wenzelm
ML_Compiler.exn_message;
20090606, by wenzelm
ML_Compiler.exn_message;
20090606, by wenzelm
added exn_message (formerly in toplevel.ML);
20090606, by wenzelm
moved Isar toplevel runtime support to runtime.ML, which is loaded early (before ml_compiler.ML);
20090606, by wenzelm
report_parse_tree: ML_open, ML_struct;
20090606, by wenzelm
export end_pos_of;
20090606, by wenzelm
use: tuned error;
20090606, by wenzelm
added markup ML_open, ML_struct;
20090606, by wenzelm
use_text: pass file name to compiler, tuned;
20090606, by wenzelm
tuned comments;
20090606, by wenzelm
removed obsolete YXML/XML.detect;
20090605, by wenzelm
Approximation: Corrected precision of ln on all real values
20090605, by hoelzl
Approximation: Implemented argument reduction for cosine. Sinus is now implemented in terms of cosine. Sqrt computes on the entire real numbers
20090604, by hoelzl
CONTRIBUTORS
20090605, by haftmann
merged
20090605, by haftmann
tuned proofs
20090605, by haftmann
added mk_valtermify_app and mk_random
20090605, by haftmann
Set.insert with authentic syntax
20090605, by haftmann
merged
20090605, by haftmann
Set.insert with authentic syntax
20090605, by haftmann
added trees implementing mappings
20090604, by haftmann
avoid Library.foldl_map
20090604, by haftmann
class replaces axclass
20090604, by haftmann
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
less
more

(0)
30000
10000
3000
1000
120
+120
+1000
+3000
+10000
+30000
tip