Mercurial
Mercurial
>
repos
>
isabelle
/ file revisions
summary
|
shortlog
|
changelog
|
graph
|
tags
|
bookmarks
|
branches
|
file
| revisions |
annotate
|
diff
|
comparison
|
rss
|
help
(0)
tip
Find changesets by keywords (author, files, the commit message), revision number or hash, or
revset expression
.
src/HOL/Fields.thy
2013-06-23
haftmann
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
file
|
diff
|
annotate
2011-09-14
huffman
tuned proofs
file
|
diff
|
annotate
2011-09-03
huffman
simplify proof
file
|
diff
|
annotate
2011-08-08
huffman
moved division ring stuff from Rings.thy to Fields.thy
file
|
diff
|
annotate
2011-05-20
hoelzl
add divide_.._cancel, inverse_.._iff
file
|
diff
|
annotate
2010-05-09
huffman
add lemmas one_less_inverse and one_le_inverse
file
|
diff
|
annotate
2010-05-06
haftmann
moved some lemmas from Groebner_Basis here
file
|
diff
|
annotate
2010-04-27
haftmann
tuned whitespace
file
|
diff
|
annotate
2010-04-27
haftmann
got rid of [simplified]
file
|
diff
|
annotate
2010-04-27
haftmann
tuned class linordered_field_inverse_zero
file
|
diff
|
annotate
2010-04-26
haftmann
use new classes (linordered_)field_inverse_zero
file
|
diff
|
annotate
2010-04-26
haftmann
dropped group_simps, ring_simps, field_eq_simps; classes division_ring_inverse_zero, field_inverse_zero, linordered_field_inverse_zero
file
|
diff
|
annotate
2010-04-25
haftmann
field_simps as named theorems
file
|
diff
|
annotate
2010-04-23
haftmann
less special treatment of times_divide_eq [simp]
file
|
diff
|
annotate
2010-04-23
haftmann
more localization; factored out lemmas for division_ring
file
|
diff
|
annotate
2010-03-18
blanchet
now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"
file
|
diff
|
annotate
2010-03-04
hoelzl
Add dense_le, dense_le_bounded, field_le_mult_one_interval.
file
|
diff
|
annotate
2010-02-18
huffman
get rid of many duplicate simp rule warnings
file
|
diff
|
annotate
2010-02-10
haftmann
moved lemma field_le_epsilon from Real.thy to Fields.thy
file
|
diff
|
annotate
2010-02-10
haftmann
moved constants inverse and divide to Ring.thy
file
|
diff
|
annotate
2010-02-08
haftmann
renamed OrderedGroup to Groups; split theory Ring_and_Field into Rings Fields
file
|
diff
|
annotate
|
base
less
more
(0)
tip