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.
Squared things out.
20070524, by obua
fix a bug : the semantics of no_asm was the opposite
20070524, by narboux
temporary fix for a bug in fresh_fun_simp
20070524, by urbanc
formalisation of my PhD (the result was correct, but the proof needed several corrections)
20070524, by urbanc
add an option in fresh_fun_simp to prevent rewriting in assumptions
20070524, by narboux
fixes tvar issue in type inference
20070524, by haftmann
tuned
20070524, by haftmann
tuned warning
20070524, by haftmann
rudimentary class target implementation
20070524, by haftmann
tuned Pure/General/name_space.ML
20070524, by haftmann
Introduced new classes monoid_add and group_add
20070524, by nipkow
add lemma complete_algebra_summable_geometric
20070523, by huffman
formatting
20070523, by paulson
generalize powerseries and termdiffs lemmas using axclasses
20070523, by huffman
remove unused simproc definition
20070523, by huffman
remove redundant simproc; remove legacy ML bindings
20070523, by huffman
remove redundant simproc
20070523, by huffman
new simp rule Infinitesimal_of_hypreal_iff
20070522, by huffman
removed redundant lemmas
20070522, by huffman
generalize uniqueness of limits to class real_normed_algebra_1
20070522, by huffman
Some hacks for SPASS format
20070522, by paulson
some optimizations, cleanup
20070522, by krauss
add missing instance declarations
20070522, by huffman
adjusted to change in Provers/Arith/combine_numerals.ML
20070522, by haftmann
adjusted to change in Provers/Arith/combine_numerals.ML
20070522, by haftmann
regression tests: send failure reports to krauss@in.tum.de, too
20070522, by krauss
rename lemmas LIM_ident, isCont_ident, DERIV_ident
20070522, by huffman
remove obsolete CSeries.thy
20070522, by huffman
generalized ring_eq_cancel simprocs to class idom; removed redundant field_eq_cancel simprocs
20070522, by huffman
new field_combine_numerals simproc, which uses fractions as coefficients
20070521, by huffman
search bottom up to get the inner fresh fun
20070521, by narboux
add a bottom up search function
20070521, by narboux
tuned
20070521, by haftmann
evaluation for integers
20070521, by haftmann
added lemma divAlg_div_mof
20070521, by haftmann
improved code for rev
20070521, by haftmann
min/max
20070521, by haftmann
generalize CombineNumerals functor to allow coefficients with types other than IntInf.int
20070521, by huffman
add lemmas divide_numeral_1 and inverse_numeral_1
20070521, by huffman
fixed signature
20070521, by krauss
Method "lexicographic_order" now takes the same arguments as "auto"
20070521, by krauss
change fresh_fun_simp to treat occurences in assumptions and try to solve the generated subgoals
20070521, by narboux
define pi with THE instead of SOME; cleaned up
20070520, by huffman
add lemmas for sin,cos,tan of 30,45,60 degrees; cleaned up
20070520, by huffman
add lemma power2_eq_imp_eq
20070520, by huffman
added lemma for permutations on strings
20070520, by urbanc
moved sqrt lemmas from Transcendental.thy to NthRoot.thy
20070520, by huffman
remove obsolete DERIV_ln lemmas
20070520, by huffman
add realpow_pos_nth2 back in
20070520, by huffman
add odd_real_root lemmas
20070520, by huffman
add lemmas about inverse functions; cleaned up proof of polar_ex
20070520, by huffman
change premises of DERIV_inverse_function lemma
20070520, by huffman
rearranged sections
20070520, by huffman
add lemmas about continuity and derivatives of roots
20070520, by huffman
add lemma DERIV_inverse_function
20070520, by huffman
add lemmas LIM_compose2, isCont_LIM_compose2
20070520, by huffman
improved aliassing
20070519, by haftmann
more robust thm handling
20070519, by haftmann
added a set of NNF normalization lemmas and nnf_conv
20070519, by chaieb
added lt and some other infix operation analogous to Ocaml's num library
20070519, by chaieb
less
more

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