| 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 |
| Wed, 18 Apr 2012 14:29:19 +0200 | hoelzl | add lemma to equate floor and div | changeset | files |
| Wed, 18 Apr 2012 14:29:18 +0200 | hoelzl | add powr_inj | changeset | files |
| Wed, 18 Apr 2012 14:29:17 +0200 | hoelzl | add lemmas to rewrite powr to power | changeset | files |
| Wed, 18 Apr 2012 14:29:16 +0200 | hoelzl | add lemmas to compare log with 0 and 1 | changeset | files |