Thu, 24 Mar 2005 17:03:37 +0100 ballarin Further work on interpretation commands. New command `interpret' for
Thu, 24 Mar 2005 16:36:40 +0100 ballarin *** empty log message ***
Thu, 24 Mar 2005 16:34:15 +0100 ballarin Transitivity reasoner ignores types amenable to linear arithmetic.
Thu, 24 Mar 2005 10:59:21 +0100 paulson COMMENT IN WRONG PLACE
Wed, 23 Mar 2005 12:09:18 +0100 paulson replaced bool by a new datatype "bit" for binary numerals
Wed, 23 Mar 2005 12:08:52 +0100 paulson temporary removal of Import
Wed, 23 Mar 2005 12:08:27 +0100 paulson tidied
Tue, 22 Mar 2005 16:32:25 +0100 paulson auto update
Tue, 22 Mar 2005 16:31:51 +0100 paulson deleted a pointless comment
Tue, 22 Mar 2005 16:30:43 +0100 paulson ensuring that "equal" is not a function
Fri, 18 Mar 2005 14:31:50 +0100 paulson auto update
Thu, 17 Mar 2005 15:12:03 +0100 paulson meson now checks that problems are first-order
Thu, 17 Mar 2005 12:19:50 +0100 nipkow added string_of_term
Thu, 17 Mar 2005 01:40:18 +0100 webertj Bugfix related to the interpretation of IDT constructors
Tue, 15 Mar 2005 17:07:41 +0100 paulson more concise ASCII escaping
Mon, 14 Mar 2005 20:30:43 +0100 huffman fixed syntax for Let <x,y> = a in e
Mon, 14 Mar 2005 17:04:10 +0100 paulson bug fixes involving typechecking clauses
Sat, 12 Mar 2005 00:07:05 +0100 huffman removed theorems about Sinl_Rep and Sinr_Rep
Fri, 11 Mar 2005 23:58:31 +0100 huffman simplified some definitions, many proofs are much shorter
Fri, 11 Mar 2005 16:56:48 +0100 webertj minor Library.option related modifications
Fri, 11 Mar 2005 16:35:06 +0100 webertj code reformatted
Fri, 11 Mar 2005 16:08:21 +0100 webertj code reformatted
Fri, 11 Mar 2005 00:45:07 +0100 huffman fixed bug: domain package can now define three or more mutually recursive types simultaneously
Fri, 11 Mar 2005 00:43:52 +0100 huffman domain package now permits indirect recursion with these type constructors: *, ->, ++, **, u
Thu, 10 Mar 2005 20:22:45 +0100 huffman fixed filename in header
Thu, 10 Mar 2005 20:19:55 +0100 huffman instance u :: (cpo) pcpo -- argument type no longer needs to be pointed
Thu, 10 Mar 2005 17:48:36 +0100 ballarin Registrations of global locale interpretations: improved, better naming.
Thu, 10 Mar 2005 09:11:57 +0100 ballarin Debugging code (error_depth) removed.
Wed, 09 Mar 2005 18:44:52 +0100 ballarin First version of global registration command.
Tue, 08 Mar 2005 16:02:52 +0100 obua fix integer overflow in numeral syntax for SML NJ.
Tue, 08 Mar 2005 00:45:58 +0100 huffman fixed variable name
Tue, 08 Mar 2005 00:32:10 +0100 huffman reordered and arranged for document generation, cleaned up some proofs
Tue, 08 Mar 2005 00:28:46 +0100 huffman removed Cprod3_lemma1 and Cprod3_lemma2
Tue, 08 Mar 2005 00:18:22 +0100 huffman reordered and arranged for document generation, cleaned up some proofs
Tue, 08 Mar 2005 00:15:01 +0100 huffman added subsection headings, cleaned up some proofs
Tue, 08 Mar 2005 00:11:49 +0100 huffman reordered and arranged for document generation, cleaned up some proofs
Tue, 08 Mar 2005 00:00:49 +0100 huffman arranged for document generation, cleaned up some proofs
Mon, 07 Mar 2005 23:54:01 +0100 huffman added subsections and text for document generation
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.
Mon, 07 Mar 2005 19:41:04 +0100 webertj HTML 4.01 Transitional conformity
Mon, 07 Mar 2005 19:30:53 +0100 webertj refute_params: default value itself=1 added (for type classes)
Mon, 07 Mar 2005 19:25:13 +0100 webertj HTML 4.01 Transitional conformity
Mon, 07 Mar 2005 19:17:07 +0100 webertj HTML 4.01 Transitional conformity
Mon, 07 Mar 2005 18:40:36 +0100 paulson now checks for higher-order vars
Mon, 07 Mar 2005 18:19:55 +0100 obua Cleaning up HOL/Matrix
Mon, 07 Mar 2005 16:55:36 +0100 paulson Tools/meson.ML: signature, structure and "open" rather than "local"
Fri, 04 Mar 2005 23:25:06 +0100 huffman add header
Fri, 04 Mar 2005 23:23:47 +0100 huffman fix headers
Fri, 04 Mar 2005 23:12:36 +0100 huffman converted to new-style theories, and combined numbered files
Fri, 04 Mar 2005 18:53:46 +0100 huffman document generation for HOLCF
Fri, 04 Mar 2005 15:07:34 +0100 skalberg Removed practically all references to Library.foldr.
Fri, 04 Mar 2005 11:44:26 +0100 paulson new first_order test
Fri, 04 Mar 2005 10:58:04 +0100 paulson removed dead code
Thu, 03 Mar 2005 17:22:46 +0100 webertj interpreter for Finite_Set.Finites added
Thu, 03 Mar 2005 12:43:01 +0100 skalberg Move towards standard functions.
Thu, 03 Mar 2005 09:22:35 +0100 nipkow fixed proof
Thu, 03 Mar 2005 01:37:32 +0100 huffman converted to new-style theory
Thu, 03 Mar 2005 00:42:04 +0100 huffman converted to new-style theory
Wed, 02 Mar 2005 23:58:02 +0100 huffman converted to new-style theory
Wed, 02 Mar 2005 23:28:17 +0100 huffman converted to new-style theory
(0) -10000 -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 +30000 tip