| Thu, 19 Apr 2012 17:32:30 +0200 | nipkow | reorganised IMP | changeset | files |
| Thu, 19 Apr 2012 11:55:30 +0200 | hoelzl | use real :: float => real as lifting-morphism so we can directlry use the rep_eq theorems | changeset | files |
| Wed, 18 Apr 2012 14:29:22 +0200 | hoelzl | use lifting to introduce floating point numbers | changeset | files |
| Wed, 18 Apr 2012 14:29:21 +0200 | hoelzl | replace the float datatype by a type with unique representation | changeset | files |
| Wed, 18 Apr 2012 14:29:20 +0200 | hoelzl | add lemmas to remove real conversions when compared to power of numerals | changeset | files |
| Wed, 18 Apr 2012 14:29:20 +0200 | hoelzl | add simp rules to rewrite comparisons of 1 and real | changeset | files |