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
hoelzl [Wed, 18 Apr 2012 14:29:21 +0200] rev 48462
replace the float datatype by a type with unique representation
hoelzl [Wed, 18 Apr 2012 14:29:20 +0200] rev 48461
add lemmas to remove real conversions when compared to power of numerals
hoelzl [Wed, 18 Apr 2012 14:29:20 +0200] rev 48460
add simp rules to rewrite comparisons of 1 and real