1998-10-15 paulson 1998-10-15 Uses overload_1st_set to specify overloading
1998-10-15 paulson 1998-10-15 specifications as sets of programs
1998-10-14 nipkow 1998-10-14 Description of new version.
1998-10-14 nipkow 1998-10-14 New many-sorted version.
1998-10-14 nipkow 1998-10-14 See (* FIXME zero_neq_conv *)
1998-10-14 nipkow 1998-10-14 Nat: added zero_neq_conv List: added nth/update lemmas.
1998-10-13 wenzelm 1998-10-13 added Int.int;
1998-10-13 wenzelm 1998-10-13 PRIVATE sig parts;
1998-10-13 paulson 1998-10-13 length_Suc_conv is no longer given to AddIffs
1998-10-13 paulson 1998-10-13 new theorems
1998-10-13 paulson 1998-10-13 tidied
1998-10-13 paulson 1998-10-13 Addition of HOL/UNITY/Client
1998-10-13 paulson 1998-10-13 new rule
1998-10-13 paulson 1998-10-13 Addition of HOL/UNITY/Client
1998-10-09 nipkow 1998-10-09 Unified treatment of type error msgs.
1998-10-09 nipkow 1998-10-09 More pretty breaks in error msgs.
1998-10-09 nipkow 1998-10-09 Added a few breaks in error text.
1998-10-09 paulson 1998-10-09 new theorem
1998-10-09 paulson 1998-10-09 new theorems
1998-10-09 paulson 1998-10-09 new guarantees laws
1998-10-09 nipkow 1998-10-09 renamed Suc_card_Diff or something
1998-10-09 nipkow 1998-10-09 Multisets at last!
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