2005-03-24 ago ballarin Further work on interpretation commands. New command `interpret' for
2005-03-24 ago ballarin *** empty log message ***
2005-03-24 ago ballarin Transitivity reasoner ignores types amenable to linear arithmetic.
2005-03-24 ago paulson COMMENT IN WRONG PLACE
2005-03-23 ago paulson replaced bool by a new datatype "bit" for binary numerals
2005-03-23 ago paulson temporary removal of Import
2005-03-23 ago paulson tidied
2005-03-22 ago paulson auto update
2005-03-22 ago paulson deleted a pointless comment
2005-03-22 ago paulson ensuring that "equal" is not a function
2005-03-18 ago paulson auto update
2005-03-17 ago paulson meson now checks that problems are first-order
2005-03-17 ago nipkow added string_of_term
2005-03-17 ago webertj Bugfix related to the interpretation of IDT constructors
2005-03-15 ago paulson more concise ASCII escaping
2005-03-14 ago huffman fixed syntax for Let <x,y> = a in e
2005-03-14 ago paulson bug fixes involving typechecking clauses
2005-03-12 ago huffman removed theorems about Sinl_Rep and Sinr_Rep
2005-03-11 ago huffman simplified some definitions, many proofs are much shorter
2005-03-11 ago webertj minor Library.option related modifications
2005-03-11 ago webertj code reformatted
2005-03-11 ago webertj code reformatted
2005-03-11 ago huffman fixed bug: domain package can now define three or more mutually recursive types simultaneously
2005-03-11 ago huffman domain package now permits indirect recursion with these type constructors: *, ->, ++, **, u
2005-03-10 ago huffman fixed filename in header
2005-03-10 ago huffman instance u :: (cpo) pcpo -- argument type no longer needs to be pointed
2005-03-10 ago ballarin Registrations of global locale interpretations: improved, better naming.
2005-03-10 ago ballarin Debugging code (error_depth) removed.
2005-03-09 ago ballarin First version of global registration command.
2005-03-08 ago obua fix integer overflow in numeral syntax for SML NJ.
2005-03-08 ago huffman fixed variable name
2005-03-08 ago huffman reordered and arranged for document generation, cleaned up some proofs
2005-03-08 ago huffman removed Cprod3_lemma1 and Cprod3_lemma2
2005-03-08 ago huffman reordered and arranged for document generation, cleaned up some proofs
2005-03-08 ago huffman added subsection headings, cleaned up some proofs
2005-03-08 ago huffman reordered and arranged for document generation, cleaned up some proofs
2005-03-08 ago huffman arranged for document generation, cleaned up some proofs
2005-03-07 ago huffman added subsections and text for document generation
2005-03-07 ago huffman Added dependency document/root.tex, and -g true option to isatool; document generation should work now.
2005-03-07 ago webertj HTML 4.01 Transitional conformity
2005-03-07 ago webertj refute_params: default value itself=1 added (for type classes)
2005-03-07 ago webertj HTML 4.01 Transitional conformity
2005-03-07 ago webertj HTML 4.01 Transitional conformity
2005-03-07 ago paulson now checks for higher-order vars
2005-03-07 ago obua Cleaning up HOL/Matrix
2005-03-07 ago paulson Tools/meson.ML: signature, structure and "open" rather than "local"
2005-03-04 ago huffman add header
2005-03-04 ago huffman fix headers
2005-03-04 ago huffman converted to new-style theories, and combined numbered files
2005-03-04 ago huffman document generation for HOLCF
2005-03-04 ago skalberg Removed practically all references to Library.foldr.
2005-03-04 ago paulson new first_order test
2005-03-04 ago paulson removed dead code
2005-03-03 ago webertj interpreter for Finite_Set.Finites added
2005-03-03 ago skalberg Move towards standard functions.
2005-03-03 ago nipkow fixed proof
2005-03-03 ago huffman converted to new-style theory
2005-03-03 ago huffman converted to new-style theory
2005-03-02 ago huffman converted to new-style theory
2005-03-02 ago huffman converted to new-style theory