| Wed, 12 Feb 2014 08:37:06 +0100 |
blanchet |
adapted to 'xxx_{case,rec}' renaming, to new theorem names, and to new variable names in theorems
|
file |
diff |
annotate
|
| Wed, 12 Feb 2014 08:35:57 +0100 |
blanchet |
renamed '{prod,sum,bool,unit}_case' to 'case_...'
|
file |
diff |
annotate
|
| Wed, 12 Feb 2014 08:35:56 +0100 |
blanchet |
adapted theories to '{case,rec}_{list,option}' names
|
file |
diff |
annotate
|
| Sun, 20 Nov 2011 21:05:23 +0100 |
wenzelm |
eliminated obsolete "standard";
|
file |
diff |
annotate
|
| Fri, 04 Nov 2011 08:19:24 +0100 |
huffman |
ex/Tree23.thy: automate proof of gfull_add
|
file |
diff |
annotate
|
| Fri, 04 Nov 2011 08:00:48 +0100 |
huffman |
ex/Tree23.thy: simplify proof of bal_del0
|
file |
diff |
annotate
|
| Fri, 04 Nov 2011 07:37:37 +0100 |
huffman |
ex/Tree23.thy: simplify proof of bal_add0
|
file |
diff |
annotate
|
| Fri, 04 Nov 2011 07:04:34 +0100 |
huffman |
ex/Tree23.thy: simpler definition of ordered-ness predicate
|
file |
diff |
annotate
|
| Thu, 03 Nov 2011 17:40:50 +0100 |
huffman |
ex/Tree23.thy: prove that deletion preserves balance
|
file |
diff |
annotate
|
| Thu, 03 Nov 2011 11:18:06 +0100 |
huffman |
ex/Tree23.thy: prove that insertion preserves tree balance and order
|
file |
diff |
annotate
|
| Sat, 23 Apr 2011 13:00:19 +0200 |
wenzelm |
modernized specifications;
|
file |
diff |
annotate
|
| Wed, 04 Nov 2009 16:54:22 +0100 |
nipkow |
New
|
file |
diff |
annotate
|