Mercurial
Mercurial
>
repos
>
isabelle
/ graph
summary

shortlog

changelog
 graph 
tags

bookmarks

branches

files

gz

help
less
more

(0)
30000
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.
modernized specifications; tuned reification
20100512, by haftmann
merged
20100512, by haftmann
added lemmas concerning last, butlast, insort
20100512, by haftmann
Remove RANGE_WARN
20100512, by Cezary Kaliszyk
clarified NEWS entry
20100512, by hoelzl
merged
20100512, by hoelzl
added NEWS entry
20100512, by hoelzl
Added atLeastAtMost_singleton_iff, atLeastAtMost_singleton'
20100511, by hoelzl
Add rules directly to the corresponding class locales instead.
20100511, by hoelzl
Removed usage of normalizating locales.
20100511, by hoelzl
speed up some proofs, fixing linarith_split_limit warnings
20100511, by huffman
fix some linarith_split_limit warnings
20100511, by huffman
include iszero_simps in semiring_norm just once (they are already included in rel_simps)
20100511, by huffman
fix duplicate simp rule warning
20100511, by huffman
no more RealPow.thy (remaining lemmas moved to RealDef.thy)
20100511, by huffman
merged
20100511, by huffman
simplify code for emptiness check
20100511, by huffman
removed lemma real_sq_order; use power2_le_imp_le instead
20100511, by huffman
merged
20100511, by haftmann
merged
20100511, by haftmann
represent deBruin indices simply by position in list
20100511, by haftmann
tuned reification functions
20100511, by haftmann
tuned code; toward a tightended interface with generated code
20100511, by haftmann
fix spelling of 'superseded'
20100511, by huffman
NEWS: removed theory PReal
20100511, by huffman
collected NEWS updates for HOLCF
20100511, by huffman
merged
20100511, by huffman
move floor lemmas from RealPow.thy to RComplete.thy
20100511, by huffman
add lemma tendsto_Complex
20100511, by huffman
move some theorems from RealPow.thy to Transcendental.thy
20100511, by huffman
add lemma power2_eq_1_iff; generalize some other lemmas
20100511, by huffman
minimize imports
20100510, by huffman
move lemma real_mult_is_one to Rings.thy, renamed to square_eq_1_iff
20100510, by huffman
clarified Pretty.font_metrics;
20100512, by wenzelm
format as topmost list of "divs", not just adjacent "spans"  for proper line breaking;
20100512, by wenzelm
tuned;
20100512, by wenzelm
more precise pretty printing based on actual font metrics;
20100511, by wenzelm
predefined spaces;
20100511, by wenzelm
merged
20100511, by wenzelm
support Isabelle plugin properties with defaults;
20100511, by wenzelm
merged
20100511, by Christian Urban
tuned proof so that no simplifier warning is printed
20100511, by Christian Urban
renamed former Int.int_induct to Int.int_of_nat_induct, former Presburger.int_induct to Int.int_induct: is more conservative and more natural than the intermediate solution
20100511, by haftmann
merged
20100511, by haftmann
tuned
20100511, by haftmann
theorem Presburger.int_induct has been renamed to Int.int_bidirectional_induct
20100511, by haftmann
tuned; dropped strange myassoc2
20100510, by haftmann
stylized COOPER exception
20100510, by haftmann
simplified oracle
20100510, by haftmann
shorten names
20100510, by haftmann
updated references to ML files
20100510, by haftmann
only one module fpr presburger method
20100510, by haftmann
moved int induction lemma to theory Int as int_bidirectional_induct
20100510, by haftmann
tuned theory text; dropped unused lemma
20100510, by haftmann
one structure is better than three
20100510, by haftmann
less complex organization of cooper source code
20100510, by haftmann
dropped unused bindings; avoid open (documents dependency on generated code more explicitly)
20100510, by haftmann
add real_mult_commute to legacy theorem names
20100510, by huffman
new construction of real numbers using Cauchy sequences
20100510, by huffman
add more credits to ex/Dedekind_Real.thy
20100510, by huffman
less
more

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