| Wed, 10 Dec 2008 17:15:26 -0800 |
huffman |
cleaned up some proofs in Cfun.thy
|
changeset |
files
|
| Wed, 10 Dec 2008 15:31:55 -0800 |
huffman |
implement cont_proc theorem cache using theory data
|
changeset |
files
|
| Wed, 10 Dec 2008 13:44:09 -0800 |
huffman |
use ML antiquotations
|
changeset |
files
|
| Wed, 10 Dec 2008 12:31:35 -0800 |
huffman |
clean up diff_bin_simps
|
changeset |
files
|
| Wed, 10 Dec 2008 07:52:54 -0800 |
huffman |
move nat_{div,mod}_distrib from NatBin to IntDiv, simplified proofs
|
changeset |
files
|
| Wed, 10 Dec 2008 23:54:03 +0100 |
wenzelm |
fixed import: requires ContNotDenum;
|
changeset |
files
|
| Wed, 10 Dec 2008 23:13:21 +0100 |
wenzelm |
fixed import: requires ContNotDenum;
|
changeset |
files
|
| Wed, 10 Dec 2008 22:46:42 +0100 |
wenzelm |
requires RComplete;
|
changeset |
files
|
| Wed, 10 Dec 2008 06:34:10 -0800 |
huffman |
merged.
|
changeset |
files
|
| Tue, 09 Dec 2008 22:13:16 -0800 |
huffman |
move all neg-related lemmas to NatBin; make type of neg specific to int
|
changeset |
files
|
| Tue, 09 Dec 2008 20:36:20 -0800 |
huffman |
separate neg_simps from rel_simps
|
changeset |
files
|
| Tue, 09 Dec 2008 20:35:31 -0800 |
huffman |
use {less,le}_number_of in integer simprocs
|
changeset |
files
|