Mercurial
isabelle
/ file revisions
summary
|
shortlog
|
changelog
|
graph
|
tags
|
branches
|
file
| revisions |
annotate
|
diff
|
rss
src/HOL/Real.thy
2014-03-06
blanchet
2014-03-06
renamed 'fun_rel' to 'rel_fun'
file
|
diff
|
annotate
2013-12-25
haftmann
2013-12-25
prefer more canonical names for lemmas on min/max
file
|
diff
|
annotate
2013-11-19
haftmann
2013-11-19
eliminiated neg_numeral in favour of - (numeral _)
file
|
diff
|
annotate
2013-11-05
hoelzl
2013-11-05
int and nat are conditionally_complete_lattices
file
|
diff
|
annotate
2013-11-05
hoelzl
2013-11-05
move Lubs from HOL to HOL-Library (replaced by conditionally complete lattices)
file
|
diff
|
annotate
2013-11-05
hoelzl
2013-11-05
generalize bdd_above/below_uminus to ordered_ab_group_add
file
|
diff
|
annotate
2013-11-05
hoelzl
2013-11-05
use bdd_above and bdd_below for conditionally complete lattices
file
|
diff
|
annotate
2013-11-01
haftmann
2013-11-01
more simplification rules on unary and binary minus
file
|
diff
|
annotate
2013-09-16
kuncar
2013-09-16
use lifting_forget for deregistering numeric types as a quotient type
file
|
diff
|
annotate
2013-09-03
wenzelm
2013-09-03
tuned proofs -- clarified flow of facts wrt. calculation;
file
|
diff
|
annotate
2013-08-18
wenzelm
2013-08-18
more symbols;
file
|
diff
|
annotate
2013-05-13
kuncar
2013-05-13
better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
file
|
diff
|
annotate
2013-04-25
hoelzl
2013-04-25
revert #916271d52466; add non-topological linear_continuum type class; show linear_continuum_topology is a perfect_space
file
|
diff
|
annotate
2013-04-24
hoelzl
2013-04-24
spell conditional_ly_-complete lattices correct
file
|
diff
|
annotate
2013-03-26
wenzelm
2013-03-26
merged
file
|
diff
|
annotate
2013-03-26
hoelzl
2013-03-26
rename RealDef to Real
file
|
diff
|
annotate
2013-03-26
hoelzl
2013-03-26
merge RComplete into RealDef
file
|
diff
|
annotate
2012-08-22
wenzelm
2012-08-22
prefer ML_file over old uses;
file
|
diff
|
annotate
2010-05-12
boehmes
2010-05-12
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
file
|
diff
|
annotate
2010-02-10
haftmann
2010-02-10
moved lemma field_le_epsilon from Real.thy to Fields.thy
file
|
diff
|
annotate
2010-02-09
haftmann
2010-02-09
simple proofs make life faster and easier
file
|
diff
|
annotate
2010-02-05
haftmann
2010-02-05
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
file
|
diff
|
annotate
2009-10-05
paulson
2009-10-05
New lemmas connected with the reals and infinite series
file
|
diff
|
annotate
2008-12-29
haftmann
2008-12-29
adapted HOL source structure to distribution layout
file
|
diff
|
annotate
2008-12-11
nipkow
2008-12-11
codegen
file
|
diff
|
annotate
2008-12-10
nipkow
2008-12-10
moved ContNotDenum into Library
file
|
diff
|
annotate
2008-12-03
haftmann
2008-12-03
made repository layout more coherent with logical distribution structure; stripped some $Id$s
file
|
diff
|
annotate
|
base