Sun, 27 Dec 2015 21:46:36 +0100 | wenzelm | prefer symbols for "floor", "ceiling"; | file | diff | annotate |
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. | file | diff | annotate |
Tue, 01 Sep 2015 22:32:58 +0200 | wenzelm | eliminated \<Colon>; | file | diff | annotate |
Mon, 25 Aug 2014 14:24:05 +0200 | hoelzl | introduce real_of typeclass for real :: 'a => real | file | diff | annotate |
Fri, 27 Apr 2012 15:24:37 +0200 | blanchet | get rid of old CASC setup and move the arithmetic part to a new theory | file | diff | annotate | base |