haftmann [Thu, 19 Apr 2012 19:18:11 +0200] rev 48472
dropped dead code
kuncar [Thu, 19 Apr 2012 18:24:40 +0200] rev 48471
rename no_code to no_abs_code - more appropriate name
kuncar [Thu, 19 Apr 2012 17:31:34 +0200] rev 48470
use tnames for bound variables in rsp thms
blanchet [Thu, 19 Apr 2012 17:49:08 +0200] rev 48469
true delayed evaluation of "SPASS_VERSION" environment variable
blanchet [Thu, 19 Apr 2012 17:49:02 +0200] rev 48468
merged
blanchet [Thu, 19 Apr 2012 11:14:57 +0200] rev 48467
use latest Z3
nipkow [Thu, 19 Apr 2012 17:32:35 +0200] rev 48466
merged
nipkow [Thu, 19 Apr 2012 17:32:30 +0200] rev 48465
reorganised IMP
hoelzl [Thu, 19 Apr 2012 11:55:30 +0200] rev 48464
use real :: float => real as lifting-morphism so we can directlry use the rep_eq theorems
hoelzl [Wed, 18 Apr 2012 14:29:22 +0200] rev 48463
use lifting to introduce floating point numbers