src/HOL/TPTP/THF_Arith.thy
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