isabelle: Graph

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

tuned
2007-05-14, by huffman
added general sum-squares lemmas
2007-05-14, by huffman
new lemmas
2007-05-14, by huffman
ProofGeneral: Find Theorems search form
2007-05-14, by webertj
reorganized float arithmetic
2007-05-14, by haftmann
fixed IntInf ambiguity
2007-05-14, by haftmann
remove redundant lemmas
2007-05-14, by huffman
remove redundant lemmas
2007-05-14, by huffman
remove redundant lemmas
2007-05-14, by huffman
remove redundant lemmas
2007-05-14, by huffman
cleaned up
2007-05-14, by huffman
tuned
2007-05-14, by huffman
define roots of negative reals so that many lemmas no longer require side conditions; simplification solves more goals than previously
2007-05-13, by huffman
add lemma power_eq_imp_eq_base
2007-05-13, by huffman
added module int
2007-05-13, by haftmann
dropped legacy
2007-05-13, by haftmann
removed module rat.ML
2007-05-13, by haftmann
whitespace tuned
2007-05-13, by haftmann
tuned
2007-05-13, by haftmann
fixed omission
2007-05-13, by haftmann
tuned setup
2007-05-13, by haftmann
refined module rat
2007-05-13, by haftmann
added modules rat.ML and int.ML
2007-05-13, by haftmann
Removed junk
2007-05-13, by nipkow
Got rid of listsp
2007-05-13, by nipkow
removed redundant lemmas
2007-05-13, by huffman
add lemma additive.setsum
2007-05-12, by huffman
*** empty log message ***
2007-05-11, by nipkow
*** empty log message ***
2007-05-11, by nipkow
proper type for fun/arg_cong_rule;
2007-05-11, by wenzelm
added fun/arg_cong_rule;
2007-05-11, by wenzelm
unified names: foo_conv;
2007-05-11, by wenzelm
tuned;
2007-05-11, by wenzelm
added fun flip f x y = f y x
2007-05-11, by krauss
generalize setsum lemmas from semiring_0_cancel to semiring_0
2007-05-11, by huffman
tuned proofs;
2007-05-11, by wenzelm
bang_facts: warning;
2007-05-11, by wenzelm
tuned proofs;
2007-05-11, by wenzelm
(class target)
2007-05-10, by haftmann
cleaned up
2007-05-10, by haftmann
beta/eta conversion after preprocessor
2007-05-10, by haftmann
fixed typo
2007-05-10, by haftmann
more conversions;
2007-05-10, by wenzelm
Moved extraction_expand declaration of listall_def outside of definition.
2007-05-10, by berghofe
Adapted to new naming scheme for definitions.
2007-05-10, by berghofe
Changed name of raw definition.
2007-05-10, by berghofe
Name of ML function "not" is now qualified in order to avoid
2007-05-10, by berghofe
consts in consts_code Isar commands are now referred to by usual term syntax
2007-05-10, by haftmann
size [nat] is identity
2007-05-10, by haftmann
explicit import of Datatype.thy due to hook bootstrap problem
2007-05-10, by haftmann
localized Sup/Inf
2007-05-10, by haftmann
localized Min/Max
2007-05-10, by haftmann
tuned
2007-05-10, by haftmann
fix proofs
2007-05-10, by huffman
remove redundant lemmas
2007-05-10, by huffman
lemmas iszero_(h)complex_number_of are no longer needed
2007-05-10, by huffman
instance real_algebra_1 < ring_char_0
2007-05-10, by huffman
new axclass ring_char_0 for rings with characteristic 0, used for of_int_eq_iff and related lemmas
2007-05-10, by huffman
moved conversions to structure Conv;
2007-05-10, by wenzelm
added dest_fun/fun2/arg1;
2007-05-10, by wenzelm

less more | (0) -10000 -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 +30000 tip

isabelle