| 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 |