1998-10-09 nipkow 1998-10-09 added Induct/Multiset*
1998-10-09 nipkow 1998-10-09 New inductive definition of `card'
1998-10-09 paulson 1998-10-09 polymorphic versions of nat_neq_iff and nat_neqE
1998-10-08 nipkow 1998-10-08 Further improvement of the simplifier.
1998-10-07 nipkow 1998-10-07 Tuned simplifier not to re-normalized already normalized terms.
1998-10-07 wenzelm 1998-10-07 tuned rm CVS;
1998-10-07 nipkow 1998-10-07 runs test
1998-10-07 paulson 1998-10-07 tidying and renaming
1998-10-07 paulson 1998-10-07 new theorems
1998-10-07 paulson 1998-10-07 tidied
1998-10-07 paulson 1998-10-07 new files UNITY/Comp.{thy,ML}
1998-10-06 nipkow 1998-10-06 Merges FoldSet into Finite
1998-10-05 paulson 1998-10-05 deleted incorrect code that set Goals.proof_timing:=false Also causes time_use_thy to set proof_timing:=true
1998-10-05 paulson 1998-10-05 Now prove_goalw_cterm never prints timing statistics
1998-10-05 paulson 1998-10-05 MLWorks demands the "op" before $
1998-10-05 paulson 1998-10-05 Finished proofs to end of section 5.1 of Chandy and Sanders
1998-10-05 paulson 1998-10-05 Join now an infix operator
1998-10-05 paulson 1998-10-05 simpler interface for Abel_Cancel
1998-10-05 paulson 1998-10-05 tidied
1998-10-02 nipkow 1998-10-02 id <-> Id
1998-10-02 paulson 1998-10-02 added Real to BasisLibrary
1998-10-02 paulson 1998-10-02 new file Provers/Arith/abel_cancel.ML
1998-10-02 paulson 1998-10-02 new files Provers/Arith/abel_cancel.ML and Real/simproc.ML
1998-10-02 paulson 1998-10-02 tidying
1998-10-01 wenzelm 1998-10-01 white border -- disabled;
1998-10-01 nipkow 1998-10-01 Improved definition of foldSet.
1998-10-01 paulson 1998-10-01 revised for new treatment of integers
1998-10-01 nipkow 1998-10-01 new singleton_conv2
1998-10-01 paulson 1998-10-01 tidied
1998-10-01 nipkow 1998-10-01 a few new lemmas.
1998-10-01 paulson 1998-10-01 composition theory
1998-10-01 paulson 1998-10-01 abstype of programs
1998-10-01 paulson 1998-10-01 now invokes functor
1998-10-01 paulson 1998-10-01 much tidying
1998-10-01 paulson 1998-10-01 new lemmas
1998-10-01 paulson 1998-10-01 better handling of literals
1998-10-01 paulson 1998-10-01 tidied
1998-10-01 paulson 1998-10-01 white space
1998-10-01 paulson 1998-10-01 new simproc functor
1998-10-01 paulson 1998-10-01 Revised version with Abelian group simprocs
1998-09-29 wenzelm 1998-09-29 handle empty name;
1998-09-29 paulson 1998-09-29 auto update
1998-09-29 paulson 1998-09-29 new function inter_term
1998-09-29 paulson 1998-09-29 Now id:(Acts prg) is implicit
1998-09-29 paulson 1998-09-29 modified proof for new simproc
1998-09-29 paulson 1998-09-29 many renamings and changes. Simproc for cancelling common terms in relations
1998-09-29 nipkow 1998-09-29 New keywords
1998-09-29 nipkow 1998-09-29 Revised wf_acc_iff and Co.
1998-09-29 nipkow 1998-09-29 new: wfUNIVI
1998-09-26 berghofe 1998-09-26 Package now chooses type variable names more carefully to avoid clashes with user-supplied type variable names.
1998-09-25 oheimb 1998-09-25 minor corrections
1998-09-25 oheimb 1998-09-25 exchanged automatic-tactics and semi-automatic-tactics added CLASET, CLASET', CLASIMPSET, CLASIMPSET'
1998-09-25 oheimb 1998-09-25 improved indentation
1998-09-25 wenzelm 1998-09-25 rearranged SIMPSET(');
1998-09-25 wenzelm 1998-09-25 *** empty log message ***
1998-09-25 wenzelm 1998-09-25 isatool logo;
1998-09-25 wenzelm 1998-09-25 added isatool logo;
1998-09-25 wenzelm 1998-09-25 improved;
1998-09-25 paulson 1998-09-25 Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
1998-09-25 paulson 1998-09-25 added Int to BasisLibrary