2005-04-06 ago quigley watcher.ML and watcher.sig changed. Debug files now write to tmp.
2005-04-05 ago quigley Current version of res_atp.ML - causes an error when I run it. C.Q.
2005-04-05 ago paulson lexicographic order by Norbert Voelker
2005-04-05 ago paulson arg_cong2 by Norbert Voelker
2005-04-05 ago nipkow *** empty log message ***
2005-04-04 ago quigley Updated to add watcher code.
2005-04-04 ago quigley CVSfj
2005-04-02 ago huffman Replaced continuity solver with new continuity simproc. Also removed cont lemmas from simp set, so that the simproc actually gets used.
2005-04-02 ago huffman converted to new-style theory
2005-04-01 ago huffman convert to new-style theory
2005-04-01 ago paulson x-symbols and other tidying
2005-04-01 ago skalberg Updated import configuration.
2005-04-01 ago gagern bring make to delete files on error
2005-04-01 ago paulson patch to get it working again
2005-03-31 ago quigley *** empty log message ***
2005-03-31 ago quigley *** empty log message ***
2005-03-31 ago quigley *** empty log message ***
2005-03-31 ago huffman added theorems eta_cfun and cont2cont_eta
2005-03-31 ago huffman chfin now a subclass of po, proved instance chfin < cpo
2005-03-31 ago huffman cleaned up some proofs
2005-03-31 ago huffman fixed bug in prj' function
2005-03-31 ago huffman changed comments to text blocks, cleaned up a few proofs
2005-03-30 ago paulson converted from DOS to UNIX format
2005-03-29 ago paulson converted HOL-Subst to tactic scripts
2005-03-28 ago paulson conversion of UNITY to Isar scripts
2005-03-26 ago paulson new display of theory stamps
2005-03-26 ago gagern op vor infix-Konstruktoren im datatype binding zum besseren Parsen
2005-03-26 ago kleing use Library/Multiset instead of own definition
2005-03-26 ago kleing fixed typo (multiset_append)
2005-03-25 ago aspinall Add askguise/informguise as best as easily possible. Prevent warning in openfile when file doesn't exist in theory database.
2005-03-25 ago paulson tidied up
2005-03-25 ago aspinall Revert previous change (but leave comments).
2005-03-25 ago aspinall Support new PGIP commands redostep, redoitem
2005-03-25 ago aspinall Support non-standard file: URL syntax, temporarily.
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