src/HOL/Library/Multiset.thy
2004-08-18 nipkow 2004-08-18 import -> imports
2004-08-16 nipkow 2004-08-16 New theory header syntax.
2004-07-22 paulson 2004-07-22 new material courtesy of Norbert Voelker
2004-06-21 kleing 2004-06-21 Merged in license change from Isabelle2004
2004-05-11 obua 2004-05-11 changes made due to new Ring_and_Field theory
2004-05-09 obua 2004-05-09 replaced apply-style proof for instance Multiset :: plus_ac0 by recommended Isar proof style
2004-05-06 wenzelm 2004-05-06 tuned document;
2004-05-01 wenzelm 2004-05-01 tuned instance statements;
2004-03-08 ballarin 2004-03-08 Bug-fixes for transitivity reasoner.
2002-09-30 berghofe 2002-09-30 Adapted to new simplifier.
2002-09-30 nipkow 2002-09-30 modified induct method
2001-12-06 wenzelm 2001-12-06 tuned;
2001-12-01 wenzelm 2001-12-01 renamed class "term" to "type" (actually "HOL.type");
2001-10-22 paulson 2001-10-22 Numerals now work for the integers: the binary numerals for 0 and 1 rewrite to their abstract counterparts, while other binary numerals work correctly.
2001-10-05 wenzelm 2001-10-05 sane numerals (stage 1): added generic 1, removed 1' and 2 on nat, "num" syntax (still with "#"), Numeral0, Numeral1;
2001-10-03 wenzelm 2001-10-03 tuned parentheses in relational expressions;
2001-09-04 wenzelm 2001-09-04 renamed "antecedent" case to "rule_context";
2001-08-06 nipkow 2001-08-06 turned translation for 1::nat into def. introduced 1' and replaced most occurrences of 1 by 1'.
2000-12-21 paulson 2000-12-21 re-orientation of 0=... (no idea why the backslashes have changed too)
2000-11-04 wenzelm 2000-11-04 tuned;
2000-10-23 wenzelm 2000-10-23 intro_classes by default; tuned;
2000-10-19 wenzelm 2000-10-19 improved typedef; tuned;
2000-10-18 wenzelm 2000-10-18 Multisets (from HOL/Induct/Multiset and friends);