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.
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
added a generic conversion for quantifier elimination and a special useful instance
20070519, by chaieb
added binop_conv, aconvc
20070519, by chaieb
added cpat antiquotation for reading certified patterns
20070519, by chaieb
unfold min/max in Stefans code generator
20070519, by nipkow
added code generation based on Isabelle's rat type.
20070519, by nipkow
Disabled Stefancs code generator  already enabled in RealDef.
20070519, by nipkow
constant op @ now named append
20070519, by haftmann
fixed comment
20070519, by haftmann
dropped legacy
20070519, by haftmann
improved eta expansion
20070519, by haftmann
dropped nonsense comment
20070519, by haftmann
fixed text
20070519, by haftmann
eliminated name clash with List.append
20070519, by haftmann
added qualification for ambiguous definition names
20070519, by haftmann
tuned
20070519, by haftmann
typ_of instance for int
20070519, by haftmann
hide locale predicate "field" from HOL library
20070519, by haftmann
no special treatment in naming of locale predicates stemming form classes
20070519, by haftmann
uniform module names for code generation
20070519, by haftmann
added Executable_Real
20070519, by haftmann
updated
20070519, by haftmann
Had to replace "case 1/2" by "case base/step". No idea why.
20070519, by nipkow
*** empty log message ***
20070519, by nipkow
remove dependence on Hilbert_Choice.thy
20070519, by huffman
use THE instead of SOME
20070519, by huffman
minimize imports
20070518, by huffman
Prove existence of nth roots using Intermediate Value Theorem
20070518, by huffman
avoid using real_mult_inverse_left; cleaned up
20070518, by huffman
use mult_strict_mono instead of real_mult_less_mono
20070518, by huffman
Fixed bug in subst causing primrec functions returning functions
20070518, by berghofe
dropped word_setup.ML
20070518, by haftmann
added files
20070517, by krauss
updated
20070517, by krauss
moved lemmas to Nat.thy
20070517, by krauss
added induction principles for induction "backwards": P (Suc n) ==> P n
20070517, by krauss
added pointer to new Unification theory
20070517, by krauss
less
more

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