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.
Added three items to the signature
20070517, by paulson
generalize some lemmas from field to division_ring
20070517, by huffman
instance division_ring < no_zero_divisors; clean up field instance proofs
20070517, by huffman
remove redundant instance declaration
20070517, by huffman
cleaned up proof of Maclaurin_sin_bound
20070517, by huffman
section labels
20070516, by huffman
minimize imports
20070516, by huffman
dropped R
20070516, by chaieb
A verified theory for rational numbers representation and simple calculations;
20070515, by chaieb
Fixed bug that caused proof of induction theorem to fail if
20070515, by berghofe
minimize imports
20070515, by huffman
clean up polar_Ex proofs; remove unnecessary lemmas
20070515, by huffman
remove simp attribute from various polar_Ex lemmas
20070515, by huffman
tuned proofs
20070514, by huffman
spelling: rename arcos > arccos
20070514, by huffman
tuned proofs
20070514, by huffman
add lemma sgn_mult; declare real_scaleR_def and scaleR_eq_0_iff as simp rules
20070514, by huffman
generalized sgn function to work on any real normed vector space
20070514, by huffman
root and sqrt on negative inputs
20070514, by huffman
move lemmas to RealPow.thy; tuned proofs
20070514, by huffman
tuned proofs
20070514, by huffman
tuned
20070514, by huffman
added general sumsquares lemmas
20070514, by huffman
new lemmas
20070514, by huffman
ProofGeneral: Find Theorems search form
20070514, by webertj
reorganized float arithmetic
20070514, by haftmann
fixed IntInf ambiguity
20070514, by haftmann
remove redundant lemmas
20070514, by huffman
remove redundant lemmas
20070514, by huffman
remove redundant lemmas
20070514, by huffman
remove redundant lemmas
20070514, by huffman
cleaned up
20070514, by huffman
tuned
20070514, by huffman
define roots of negative reals so that many lemmas no longer require side conditions; simplification solves more goals than previously
20070513, by huffman
add lemma power_eq_imp_eq_base
20070513, by huffman
added module int
20070513, by haftmann
dropped legacy
20070513, by haftmann
removed module rat.ML
20070513, by haftmann
whitespace tuned
20070513, by haftmann
tuned
20070513, by haftmann
fixed omission
20070513, by haftmann
tuned setup
20070513, by haftmann
refined module rat
20070513, by haftmann
added modules rat.ML and int.ML
20070513, by haftmann
Removed junk
20070513, by nipkow
Got rid of listsp
20070513, by nipkow
removed redundant lemmas
20070513, by huffman
add lemma additive.setsum
20070512, by huffman
*** empty log message ***
20070511, by nipkow
*** empty log message ***
20070511, by nipkow
proper type for fun/arg_cong_rule;
20070511, by wenzelm
added fun/arg_cong_rule;
20070511, by wenzelm
unified names: foo_conv;
20070511, by wenzelm
tuned;
20070511, by wenzelm
added fun flip f x y = f y x
20070511, by krauss
generalize setsum lemmas from semiring_0_cancel to semiring_0
20070511, by huffman
tuned proofs;
20070511, by wenzelm
bang_facts: warning;
20070511, by wenzelm
tuned proofs;
20070511, by wenzelm
(class target)
20070510, by haftmann
less
more

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