1998-10-19 mueller 1998-10-19 solved conflict by taking newest version;
1998-10-19 paulson 1998-10-19 added Clarify_tac to speed up proofs
1998-10-19 paulson 1998-10-19 moved a theorem
1998-10-19 paulson 1998-10-19 fixed comment
1998-10-19 paulson 1998-10-19 fixed some indenting; changed a VERY slow blast_tac to fast_tac
1998-10-18 wenzelm 1998-10-18 updated, tuned;
1998-10-18 wenzelm 1998-10-18 added Minho (Portugal);
1998-10-16 berghofe 1998-10-16 Fixed bug (improper handling of flag flat_names).
1998-10-16 berghofe 1998-10-16 Added quiet_mode flag.
1998-10-16 berghofe 1998-10-16 - Changed structure of name spaces - Proofs for datatypes with unneeded parameters are working now - added additional parameter flat_names - added quiet_mode flag
1998-10-16 wenzelm 1998-10-16 tuned MLWorks options; added print_depth;
1998-10-16 wenzelm 1998-10-16 MLWorks 2.0;
1998-10-16 berghofe 1998-10-16 Changed structure of name spaces for datatypes.
1998-10-16 nipkow 1998-10-16 2. The simplifier now knows a little bit about nat-arithmetic.
1998-10-16 nipkow 1998-10-16 Mods because trans_tac is now part of thge simplifier.
1998-10-16 nipkow 1998-10-16 Mods because of: Installed trans_tac in solver of simpset().
1998-10-16 nipkow 1998-10-16 Installed trans_tac in solver of simpset().
1998-10-16 paulson 1998-10-16 changed tags from 0, 1 to None, Some() to avoid special treatment of 0
1998-10-16 paulson 1998-10-16 parent is Main
1998-10-16 nipkow 1998-10-16 *** empty log message ***
1998-10-15 paulson 1998-10-15 integer simprocs
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