2005-05-17 wenzelm 2005-05-17 added;
2005-05-17 wenzelm 2005-05-17 proper treatment of directory links; tuned;
2005-05-17 kleing 2005-05-17 use Drule.vars_of_terms
2005-05-16 paulson 2005-05-16 Use of IntInf.int instead of int in most numeric simprocs; avoids integer overflow in SML/NJ
2005-05-16 kleing 2005-05-16 searching for thms by combination of criteria (intro, elim, dest, name, term pattern)
2005-05-16 kleing 2005-05-16 export parser for "-"
2005-05-16 kleing 2005-05-16 line wrap
2005-05-15 berghofe 2005-05-15 Eta-expanded merge function (to make SmlNJ happy).
2005-05-14 haftmann 2005-05-14 added Proof.context to antiquotation
2005-05-13 dixon 2005-05-13 lucas - fixed bug with uninstantiated type contexts in eqsubst and added the automatic removal of duplicate subgoals (when there are no flex-flex constraints)
2005-05-13 nipkow 2005-05-13 -(n::nat) is now regarded as atomic
2005-05-13 schirmer 2005-05-13 Bugfix in syntax translation for record type.
2005-05-12 paulson 2005-05-12 theorem names for caching
2005-05-12 paulson 2005-05-12 memoization of ResAxioms.cnf_axiom rather than of Reconstruction.clausify_rule
2005-05-12 paulson 2005-05-12 first-order now ignores "all"
2005-05-12 nipkow 2005-05-12 fixed a few things and added Haftmann as author
2005-05-11 paulson 2005-05-11 documented new subst method
2005-05-11 haftmann 2005-05-11 corrections
2005-05-11 nipkow 2005-05-11 Added thms by Brian Huffmann
2005-05-10 paulson 2005-05-10 new cterm primitives
2005-05-10 paulson 2005-05-10 oops...cannot use subst here
2005-05-10 kleing 2005-05-10 table centering, headline 'other platform'
2005-05-09 paulson 2005-05-09 unfolding of Ex1
2005-05-09 paulson 2005-05-09 choice_const moved to hologic.ML
2005-05-09 paulson 2005-05-09 from simplesubst to new subst
2005-05-09 haftmann 2005-05-09 minor corrections
2005-05-09 kleing 2005-05-09 made file links local, smoothed text over in some places
2005-05-09 kleing 2005-05-09 made file list nicer
2005-05-09 kleing 2005-05-09 moved description (dist area) out of link
2005-05-09 kleing 2005-05-09 made download links local, provide explicit list of files to download
2005-05-09 kleing 2005-05-09 shortened
2005-05-08 wenzelm 2005-05-08 MAILTO: makarius@sketis.net
2005-05-06 dixon 2005-05-06 lucas - added ability to provide multiple replacements for subst: syntax is now: subst (1 3) myrule
2005-05-06 haftmann 2005-05-06 added notes for mac os
2005-05-06 haftmann 2005-05-06 Added notes for installation on Windows
2005-05-06 haftmann 2005-05-06 added option 'tidy=' to makefile, for optional processing of results by HTML tidy
2005-05-06 haftmann 2005-05-06 replaced some outdated HTML by more modern constructs
2005-05-06 haftmann 2005-05-06 added new antiquotations
2005-05-06 huffman 2005-05-06 Replaced all unnecessary uses of SOME with THE or LEAST
2005-05-05 dixon 2005-05-05 lucas - added option to select occurance to rewrite e.g. (occ 4)
2005-05-05 dixon 2005-05-05 lucas - made clean unify smash unifiers so that when we get flex-flex constraints subst does not barf. Also added fix_vars_upto_idx to IsaND.
2005-05-05 dixon 2005-05-05 lucas - added update node function.
2005-05-04 berghofe 2005-05-04 Added eta_long attribute.
2005-05-04 berghofe 2005-05-04 Added eta_long_conversion.
2005-05-04 paulson 2005-05-04 eta-expansion
2005-05-04 nipkow 2005-05-04 fixed lin.arith
2005-05-04 nipkow 2005-05-04 neqE applies even if the type is not one which partakes in linear arithmetic. This lead to confusion. Now there are multiple type specific neqE.
2005-05-04 nipkow 2005-05-04 Fixing a problem with lin.arith.
2005-05-03 haftmann 2005-05-03 make mkdir usable with cygwin
2005-05-03 quigley 2005-05-03 Replaced reference to SPASS with general one - set SPASS_HOME in settings file. Rewrote res_clasimpset.ML. Now produces an array of (thm, clause) in addition to writing out clasimpset as tptp strings. C.Q.
2005-05-03 haftmann 2005-05-03 final implementation of antiquotations styles
2005-05-03 haftmann 2005-05-03 Added short description of thm_style and term_style antiquotation
2005-05-03 nipkow 2005-05-03 *** empty log message ***
2005-05-03 dixon 2005-05-03 lucas - improved interface to isand.ML and cleaned up clean-unification code, and added some better comments.
2005-05-03 dixon 2005-05-03 lucas - added dest_TVar and dest_TFree.
2005-05-02 schirmer 2005-05-02 Removed nodup_vars avoiding hack
2005-05-02 nipkow 2005-05-02 fixed
2005-05-02 nipkow 2005-05-02 turned 2 lemmas into simp rules
2005-05-02 nipkow 2005-05-02 *** empty log message ***
2005-05-02 nipkow 2005-05-02 fixed setsum problem