| Wed, 23 Mar 2005 12:08:52 +0100 |
paulson |
temporary removal of Import
|
changeset |
files
|
| Wed, 23 Mar 2005 12:08:27 +0100 |
paulson |
tidied
|
changeset |
files
|
| Tue, 22 Mar 2005 16:32:25 +0100 |
paulson |
auto update
|
changeset |
files
|
| Tue, 22 Mar 2005 16:31:51 +0100 |
paulson |
deleted a pointless comment
|
changeset |
files
|
| Tue, 22 Mar 2005 16:30:43 +0100 |
paulson |
ensuring that "equal" is not a function
|
changeset |
files
|
| Fri, 18 Mar 2005 14:31:50 +0100 |
paulson |
auto update
|
changeset |
files
|
| Thu, 17 Mar 2005 15:12:03 +0100 |
paulson |
meson now checks that problems are first-order
|
changeset |
files
|
| Thu, 17 Mar 2005 12:19:50 +0100 |
nipkow |
added string_of_term
|
changeset |
files
|
| Thu, 17 Mar 2005 01:40:18 +0100 |
webertj |
Bugfix related to the interpretation of IDT constructors
|
changeset |
files
|
| Tue, 15 Mar 2005 17:07:41 +0100 |
paulson |
more concise ASCII escaping
|
changeset |
files
|
| Mon, 14 Mar 2005 20:30:43 +0100 |
huffman |
fixed syntax for Let <x,y> = a in e
|
changeset |
files
|
| Mon, 14 Mar 2005 17:04:10 +0100 |
paulson |
bug fixes involving typechecking clauses
|
changeset |
files
|
| Sat, 12 Mar 2005 00:07:05 +0100 |
huffman |
removed theorems about Sinl_Rep and Sinr_Rep
|
changeset |
files
|
| Fri, 11 Mar 2005 23:58:31 +0100 |
huffman |
simplified some definitions, many proofs are much shorter
|
changeset |
files
|
| Fri, 11 Mar 2005 16:56:48 +0100 |
webertj |
minor Library.option related modifications
|
changeset |
files
|
| Fri, 11 Mar 2005 16:35:06 +0100 |
webertj |
code reformatted
|
changeset |
files
|
| Fri, 11 Mar 2005 16:08:21 +0100 |
webertj |
code reformatted
|
changeset |
files
|
| Fri, 11 Mar 2005 00:45:07 +0100 |
huffman |
fixed bug: domain package can now define three or more mutually recursive types simultaneously
|
changeset |
files
|
| Fri, 11 Mar 2005 00:43:52 +0100 |
huffman |
domain package now permits indirect recursion with these type constructors: *, ->, ++, **, u
|
changeset |
files
|
| Thu, 10 Mar 2005 20:22:45 +0100 |
huffman |
fixed filename in header
|
changeset |
files
|
| Thu, 10 Mar 2005 20:19:55 +0100 |
huffman |
instance u :: (cpo) pcpo -- argument type no longer needs to be pointed
|
changeset |
files
|
| Thu, 10 Mar 2005 17:48:36 +0100 |
ballarin |
Registrations of global locale interpretations: improved, better naming.
|
changeset |
files
|
| Thu, 10 Mar 2005 09:11:57 +0100 |
ballarin |
Debugging code (error_depth) removed.
|
changeset |
files
|
| Wed, 09 Mar 2005 18:44:52 +0100 |
ballarin |
First version of global registration command.
|
changeset |
files
|
| Tue, 08 Mar 2005 16:02:52 +0100 |
obua |
fix integer overflow in numeral syntax for SML NJ.
|
changeset |
files
|
| Tue, 08 Mar 2005 00:45:58 +0100 |
huffman |
fixed variable name
|
changeset |
files
|
| Tue, 08 Mar 2005 00:32:10 +0100 |
huffman |
reordered and arranged for document generation, cleaned up some proofs
|
changeset |
files
|
| Tue, 08 Mar 2005 00:28:46 +0100 |
huffman |
removed Cprod3_lemma1 and Cprod3_lemma2
|
changeset |
files
|
| Tue, 08 Mar 2005 00:18:22 +0100 |
huffman |
reordered and arranged for document generation, cleaned up some proofs
|
changeset |
files
|
| Tue, 08 Mar 2005 00:15:01 +0100 |
huffman |
added subsection headings, cleaned up some proofs
|
changeset |
files
|
| Tue, 08 Mar 2005 00:11:49 +0100 |
huffman |
reordered and arranged for document generation, cleaned up some proofs
|
changeset |
files
|
| Tue, 08 Mar 2005 00:00:49 +0100 |
huffman |
arranged for document generation, cleaned up some proofs
|
changeset |
files
|
| Mon, 07 Mar 2005 23:54:01 +0100 |
huffman |
added subsections and text for document generation
|
changeset |
files
|
| Mon, 07 Mar 2005 23:30:06 +0100 |
huffman |
Added dependency document/root.tex, and -g true option to isatool; document generation should work now.
|
changeset |
files
|
| Mon, 07 Mar 2005 19:41:04 +0100 |
webertj |
HTML 4.01 Transitional conformity
|
changeset |
files
|
| Mon, 07 Mar 2005 19:30:53 +0100 |
webertj |
refute_params: default value itself=1 added (for type classes)
|
changeset |
files
|
| Mon, 07 Mar 2005 19:25:13 +0100 |
webertj |
HTML 4.01 Transitional conformity
|
changeset |
files
|
| Mon, 07 Mar 2005 19:17:07 +0100 |
webertj |
HTML 4.01 Transitional conformity
|
changeset |
files
|
| Mon, 07 Mar 2005 18:40:36 +0100 |
paulson |
now checks for higher-order vars
|
changeset |
files
|
| Mon, 07 Mar 2005 18:19:55 +0100 |
obua |
Cleaning up HOL/Matrix
|
changeset |
files
|
| Mon, 07 Mar 2005 16:55:36 +0100 |
paulson |
Tools/meson.ML: signature, structure and "open" rather than "local"
|
changeset |
files
|
| Fri, 04 Mar 2005 23:25:06 +0100 |
huffman |
add header
|
changeset |
files
|
| Fri, 04 Mar 2005 23:23:47 +0100 |
huffman |
fix headers
|
changeset |
files
|
| Fri, 04 Mar 2005 23:12:36 +0100 |
huffman |
converted to new-style theories, and combined numbered files
|
changeset |
files
|
| Fri, 04 Mar 2005 18:53:46 +0100 |
huffman |
document generation for HOLCF
|
changeset |
files
|
| Fri, 04 Mar 2005 15:07:34 +0100 |
skalberg |
Removed practically all references to Library.foldr.
|
changeset |
files
|
| Fri, 04 Mar 2005 11:44:26 +0100 |
paulson |
new first_order test
|
changeset |
files
|
| Fri, 04 Mar 2005 10:58:04 +0100 |
paulson |
removed dead code
|
changeset |
files
|
| Thu, 03 Mar 2005 17:22:46 +0100 |
webertj |
interpreter for Finite_Set.Finites added
|
changeset |
files
|
| Thu, 03 Mar 2005 12:43:01 +0100 |
skalberg |
Move towards standard functions.
|
changeset |
files
|
| Thu, 03 Mar 2005 09:22:35 +0100 |
nipkow |
fixed proof
|
changeset |
files
|
| Thu, 03 Mar 2005 01:37:32 +0100 |
huffman |
converted to new-style theory
|
changeset |
files
|
| Thu, 03 Mar 2005 00:42:04 +0100 |
huffman |
converted to new-style theory
|
changeset |
files
|
| Wed, 02 Mar 2005 23:58:02 +0100 |
huffman |
converted to new-style theory
|
changeset |
files
|
| Wed, 02 Mar 2005 23:28:17 +0100 |
huffman |
converted to new-style theory
|
changeset |
files
|
| Wed, 02 Mar 2005 23:15:16 +0100 |
huffman |
converted to new-style theory
|
changeset |
files
|
| Wed, 02 Mar 2005 22:57:08 +0100 |
huffman |
converted to new-style theory
|
changeset |
files
|
| Wed, 02 Mar 2005 22:30:00 +0100 |
huffman |
converted to new-style theory
|
changeset |
files
|
| Wed, 02 Mar 2005 12:06:15 +0100 |
nipkow |
another reorganization of setsums and intervals
|
changeset |
files
|
| Wed, 02 Mar 2005 10:33:10 +0100 |
dixon |
lucas - fixed bug with name capture variables bound outside redex could (previously)conflict with scheme variables that occur in the conditions of an equation, and which were renamed to avoid conflict with another instantiation. This has now been fixed.
|
changeset |
files
|