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
2013-04-25 hoelzl 2013-04-25 revert #916271d52466; add non-topological linear_continuum type class; show linear_continuum_topology is a perfect_space
2013-04-24 hoelzl 2013-04-24 spell conditional_ly_-complete lattices correct
2013-03-26 wenzelm 2013-03-26 merged
2013-03-26 hoelzl 2013-03-26 rename RealDef to Real
2013-03-26 hoelzl 2013-03-26 merge RComplete into RealDef
2012-08-22 wenzelm 2012-08-22 prefer ML_file over old uses;
2010-05-12 boehmes 2010-05-12 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
2010-02-10 haftmann 2010-02-10 moved lemma field_le_epsilon from Real.thy to Fields.thy
2010-02-09 haftmann 2010-02-09 simple proofs make life faster and easier
2010-02-05 haftmann 2010-02-05 more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
2009-10-05 paulson 2009-10-05 New lemmas connected with the reals and infinite series
2008-12-29 haftmann 2008-12-29 adapted HOL source structure to distribution layout
2008-12-11 nipkow 2008-12-11 codegen
2008-12-10 nipkow 2008-12-10 moved ContNotDenum into Library
2008-12-03 haftmann 2008-12-03 made repository layout more coherent with logical distribution structure; stripped some $Id$s