src/HOL/TPTP/THF_Arith.thy
Sun, 27 Dec 2015 21:46:36 +0100 wenzelm prefer symbols for "floor", "ceiling";
Tue, 10 Nov 2015 14:18:41 +0000 paulson Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
Tue, 01 Sep 2015 22:32:58 +0200 wenzelm eliminated \<Colon>;
Mon, 25 Aug 2014 14:24:05 +0200 hoelzl introduce real_of typeclass for real :: 'a => real
Fri, 27 Apr 2012 15:24:37 +0200 blanchet get rid of old CASC setup and move the arithmetic part to a new theory
less more (0) tip