src/HOL/TPTP/THF_Arith.thy
2015-12-27 wenzelm 2015-12-27 prefer symbols for "floor", "ceiling";
2015-11-10 paulson 2015-11-10 Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
2015-09-01 wenzelm 2015-09-01 eliminated \<Colon>;
2014-08-25 hoelzl 2014-08-25 introduce real_of typeclass for real :: 'a => real
2012-04-27 blanchet 2012-04-27 get rid of old CASC setup and move the arithmetic part to a new theory