Thu, 10 Dec 2009 03:25:42 +0100 |
Christian Urban |
merged
|
changeset |
files
|
Thu, 10 Dec 2009 03:11:19 +0100 |
Christian Urban |
simplified proofs
|
changeset |
files
|
Thu, 10 Dec 2009 02:46:08 +0100 |
Christian Urban |
removed quot_respect attribute of a non-standard lemma
|
changeset |
files
|
Thu, 10 Dec 2009 02:42:09 +0100 |
Cezary Kaliszyk |
With int_of_nat as a quotient_def, lemmas about it can be easily lifted.
|
changeset |
files
|
Thu, 10 Dec 2009 01:48:39 +0100 |
Christian Urban |
merged
|
changeset |
files
|
Thu, 10 Dec 2009 01:47:55 +0100 |
Christian Urban |
naming in this file cannot be made to agree to the original (PROBLEM?)
|
changeset |
files
|
Thu, 10 Dec 2009 01:39:47 +0100 |
Cezary Kaliszyk |
Lifted some kind of induction.
|
changeset |
files
|
Wed, 09 Dec 2009 23:32:16 +0100 |
Christian Urban |
more proofs in IntEx2
|
changeset |
files
|
Wed, 09 Dec 2009 22:43:11 +0100 |
Cezary Kaliszyk |
Finished one proof in IntEx2.
|
changeset |
files
|
Wed, 09 Dec 2009 22:05:11 +0100 |
Christian Urban |
slightly more on IntEx2
|
changeset |
files
|
Wed, 09 Dec 2009 20:35:52 +0100 |
Christian Urban |
proved (with a lot of pain) that times_raw is respectful
|
changeset |
files
|
Wed, 09 Dec 2009 17:31:19 +0100 |
Christian Urban |
merged
|
changeset |
files
|
Wed, 09 Dec 2009 17:31:01 +0100 |
Christian Urban |
fixed minor stupidity
|
changeset |
files
|
Wed, 09 Dec 2009 17:16:39 +0100 |
Cezary Kaliszyk |
Exception handling.
|
changeset |
files
|
Wed, 09 Dec 2009 17:05:33 +0100 |
Cezary Kaliszyk |
Code cleaning.
|
changeset |
files
|