src/HOL/Library/Multiset.thy
Tue, 23 Nov 2004 16:43:03 +0100 nipkow renamed 1 lemmas
Wed, 18 Aug 2004 11:09:40 +0200 nipkow import -> imports
Mon, 16 Aug 2004 14:22:27 +0200 nipkow New theory header syntax.
Thu, 22 Jul 2004 10:33:26 +0200 paulson new material courtesy of Norbert Voelker
Mon, 21 Jun 2004 10:25:57 +0200 kleing Merged in license change from Isabelle2004
Tue, 11 May 2004 20:11:08 +0200 obua changes made due to new Ring_and_Field theory
Sun, 09 May 2004 23:04:36 +0200 obua replaced apply-style proof for instance Multiset :: plus_ac0 by recommended Isar proof style
Thu, 06 May 2004 14:14:18 +0200 wenzelm tuned document;
Sat, 01 May 2004 22:01:57 +0200 wenzelm tuned instance statements;
Mon, 08 Mar 2004 12:17:43 +0100 ballarin Bug-fixes for transitivity reasoner.
Mon, 30 Sep 2002 16:14:02 +0200 berghofe Adapted to new simplifier.
Mon, 30 Sep 2002 15:44:21 +0200 nipkow modified induct method
Thu, 06 Dec 2001 00:40:19 +0100 wenzelm tuned;
Sat, 01 Dec 2001 18:52:32 +0100 wenzelm renamed class "term" to "type" (actually "HOL.type");
Mon, 22 Oct 2001 11:54:22 +0200 paulson Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
Fri, 05 Oct 2001 21:52:39 +0200 wenzelm sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
Wed, 03 Oct 2001 20:54:16 +0200 wenzelm tuned parentheses in relational expressions;
Tue, 04 Sep 2001 21:10:57 +0200 wenzelm renamed "antecedent" case to "rule_context";
Mon, 06 Aug 2001 13:43:24 +0200 nipkow turned translation for 1::nat into def.
Thu, 21 Dec 2000 10:16:07 +0100 paulson re-orientation of 0=... (no idea why the backslashes have changed too)
Sat, 04 Nov 2000 18:41:37 +0100 wenzelm tuned;
Mon, 23 Oct 2000 22:17:55 +0200 wenzelm intro_classes by default;
Thu, 19 Oct 2000 21:22:44 +0200 wenzelm improved typedef;
Wed, 18 Oct 2000 23:28:33 +0200 wenzelm Multisets (from HOL/Induct/Multiset and friends);
less more (0) tip