| Thu, 09 Oct 2003 18:13:32 +0200 |
skalberg |
Added support for making constants final, that is, ensuring that no
|
file |
diff |
annotate
|
| Wed, 08 Oct 2003 16:02:54 +0200 |
skalberg |
Added axiomatic specifications (ax_specification).
|
file |
diff |
annotate
|
| Wed, 27 Aug 2003 10:11:30 +0200 |
skalberg |
Improved the error messages (slightly).
|
file |
diff |
annotate
|
| Tue, 26 Aug 2003 19:33:35 +0200 |
skalberg |
Cleaned up the code.
|
file |
diff |
annotate
|
| Tue, 26 Aug 2003 18:49:17 +0200 |
skalberg |
Allowed for splitting the specification over several lemmas.
|
file |
diff |
annotate
|
| Mon, 21 Jul 2003 17:27:23 +0200 |
skalberg |
Added handling of meta implication and meta quantification.
|
file |
diff |
annotate
|
| Mon, 21 Jul 2003 16:19:34 +0200 |
skalberg |
Added handling of free variables (provided they are of sort HOL.type).
|
file |
diff |
annotate
|
| Mon, 21 Jul 2003 08:53:56 +0200 |
skalberg |
Changed bstring argument to xstring.
|
file |
diff |
annotate
|
| Mon, 21 Jul 2003 08:52:06 +0200 |
skalberg |
*** empty log message ***
|
file |
diff |
annotate
|
| Sat, 19 Jul 2003 17:35:15 +0200 |
skalberg |
Added optional theorem names for the constant definitions added during
|
file |
diff |
annotate
|
| Thu, 17 Jul 2003 15:23:20 +0200 |
skalberg |
Added package for definition by specification.
|
file |
diff |
annotate
|