| Fri, 26 Feb 2010 08:37:03 -0800 |
huffman |
move proof of compactness rules into domain_constructors.ML
|
changeset |
files
|
| Fri, 26 Feb 2010 07:17:29 -0800 |
huffman |
add some convenience functions
|
changeset |
files
|
| Thu, 25 Feb 2010 13:16:28 -0800 |
huffman |
rewrite domain package code for selector functions
|
changeset |
files
|
| Wed, 24 Feb 2010 17:37:59 -0800 |
huffman |
add function beta_of_def
|
changeset |
files
|
| Wed, 24 Feb 2010 16:15:03 -0800 |
huffman |
reorganizing domain package code (in progress)
|
changeset |
files
|
| Wed, 24 Feb 2010 14:20:07 -0800 |
huffman |
change domain package's treatment of variable names in theorems to be like datatype package
|
changeset |
files
|
| Wed, 24 Feb 2010 14:13:15 -0800 |
huffman |
remove redundant lemma real_minus_half_eq
|
changeset |
files
|
| Wed, 24 Feb 2010 10:36:17 -0800 |
huffman |
polished and converted some proofs to Isar style
|
changeset |
files
|
| Tue, 02 Mar 2010 12:26:50 +0100 |
krauss |
killed more recdefs
|
changeset |
files
|
| Mon, 01 Mar 2010 18:49:55 +0100 |
krauss |
tuned comment
|
changeset |
files
|
| Tue, 02 Mar 2010 09:05:50 +0100 |
haftmann |
repaired subscripts broken in d8d7d1b785af
|
changeset |
files
|
| Tue, 02 Mar 2010 08:28:06 +0100 |
haftmann |
repaired definition (cf. d8d7d1b785af)
|
changeset |
files
|