Mercurial
Mercurial
>
repos
>
isabelle
/ graph
summary

shortlog

changelog
 graph 
tags

bookmarks

branches

files

gz

help
less
more

(0)
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.
Compatibility wrapper for Poly/ML 4.9.1.
20060927, by wenzelm
removed all references to star_n and FreeUltrafilterNat
20060927, by huffman
add lemmas about hnorm, Infinitesimal
20060927, by huffman
reverted to 1.58;
20060927, by wenzelm
proper const_syntax for uminus, abs;
20060927, by wenzelm
reorganized HNatInfinite proofs; simplified and renamed some lemmas
20060927, by huffman
removed obsolete of_instream_slurp  now already included in tty;
20060927, by wenzelm
Source.tty now slurps by default;
20060927, by wenzelm
of_stream/tty: slurp input eagerly;
20060927, by wenzelm
tuned all_paths;
20060927, by wenzelm
internal params: Vartab instead of AList;
20060927, by wenzelm
removed unused serial_of, name_of;
20060927, by wenzelm
removed redundant lemmas;
20060927, by wenzelm
remove redundant lemmas
20060927, by huffman
replaced constant 0 by HOL.zero
20060927, by haftmann
hypreal_of_nat abbreviates of_nat
20060927, by huffman
add lemmas of_real_eq_star_of, Reals_eq_Standard
20060927, by huffman
move star_of_norm from SEQ.thy to NSA.thy
20060927, by huffman
convert more proofs to transfer principle
20060927, by huffman
add lemmas about Standard, real_of, scaleR
20060927, by huffman
instance complex :: real_normed_field; cleaned up
20060927, by huffman
add lemma stc_unique; shorten stc proofs
20060927, by huffman
add lemmas approx_diff and st_unique, shorten st proofs
20060927, by huffman
add lemmas about of_real and power
20060927, by huffman
reorganize section headings
20060927, by huffman
more lemmas about Standard and star_of
20060927, by huffman
define new constant Standard = range star_of
20060927, by huffman
add lemmas of_int_in_Reals, of_nat_in_Reals
20060927, by huffman
add header
20060926, by huffman
Changed precedence of "op O" (relation composition) from 60 to 75.
20060926, by krauss
handling of \<^const> syntax for case; explicit case names for induction rules for rep_datatype
20060926, by haftmann
tuned syntax for <= <
20060926, by haftmann
renamed 0 and 1 to HOL.zero and HOL.one respectivly; introduced corresponding syntactic classes
20060926, by haftmann
renamed 0 and 1 to HOL.zero and HOL.one respectivly
20060926, by haftmann
fixed the definition of "depth"
20060926, by paulson
Abstraction now handles equations where the RHS is a lambdaexpression; also, strings of lambdas
20060926, by paulson
some cleanup
20060925, by haftmann
changed order
20060925, by haftmann
inserted headings
20060925, by haftmann
changed interface in codegen_package.ML
20060925, by haftmann
fixed some mess
20060925, by haftmann
cleaned up
20060925, by haftmann
adding constants the modern way
20060925, by haftmann
added examples for variable name handling
20060925, by haftmann
better handling for div by zero
20060925, by haftmann
updated theory description
20060925, by haftmann
refinements in codegen serializer
20060925, by haftmann
added 'undefined' serializer
20060925, by haftmann
added code_instname
20060925, by haftmann
reorganized subsection headings
20060924, by huffman
moved SEQ_Infinitesimal from SEQ to HyperNat
20060924, by huffman
real_norm_def [simp]
20060924, by huffman
generalize types of lim and nslim
20060924, by huffman
generalized types of sums, summable, and suminf
20060924, by huffman
add lemma convergent_Cauchy
20060924, by huffman
remove extra dependencies
20060924, by huffman
add proof of summable_LIMSEQ_zero
20060924, by huffman
change definitions from SOME to THE
20060924, by huffman
move root and sqrt stuff from Transcendental to NthRoot
20060924, by huffman
fix proof
20060924, by huffman
less
more

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