| Tue, 12 Jul 2005 18:44:32 +0200 |
huffman |
changed orientation of bind_assoc rule
|
file |
diff |
annotate
|
| Tue, 12 Jul 2005 18:20:44 +0200 |
huffman |
generalized types of monadic operators to class cpo; added match function for UU
|
file |
diff |
annotate
|
| Fri, 08 Jul 2005 03:12:58 +0200 |
huffman |
fix typo
|
file |
diff |
annotate
|
| Fri, 08 Jul 2005 02:41:35 +0200 |
huffman |
renamed upE1 to upE
|
file |
diff |
annotate
|
| Thu, 23 Jun 2005 21:17:26 +0200 |
huffman |
added match functions for spair, sinl, sinr
|
file |
diff |
annotate
|
| Sat, 18 Jun 2005 00:38:18 +0200 |
huffman |
fixrec shows unsolved subgoals when proofs of rewrites fail
|
file |
diff |
annotate
|
| Fri, 17 Jun 2005 18:50:40 +0200 |
huffman |
added match functions for ONE, TT, and FF; added theorem mplus_fail2
|
file |
diff |
annotate
|
| Fri, 17 Jun 2005 16:12:49 +0200 |
haftmann |
migrated theory headers to new format
|
file |
diff |
annotate
|
| Wed, 15 Jun 2005 20:50:38 +0200 |
huffman |
fixrec package now handles mutually-recursive definitions
|
file |
diff |
annotate
|
| Sat, 04 Jun 2005 02:11:47 +0200 |
huffman |
use fixrec_package.ML
|
file |
diff |
annotate
|
| Sat, 04 Jun 2005 00:22:08 +0200 |
huffman |
New theory with lemmas for the fixrec package
|
file |
diff |
annotate
|