src/HOL/NumberTheory/BijectionRel.thy
2007-07-11 berghofe 2007-07-11 Adapted to new inductive definition package.
2007-02-07 berghofe 2007-02-07 Adapted to changes in Finite_Set theory.
2006-11-17 wenzelm 2006-11-17 more robust syntax for definition/abbreviation/notation;
2006-05-17 wenzelm 2006-05-17 prefer 'definition' over low-level defs; tuned source/document;
2005-12-08 wenzelm 2005-12-08 tuned sources and proofs
2005-06-17 haftmann 2005-06-17 migrated theory headers to new format
2002-10-08 nipkow 2002-10-08 Got rid of rotates because of new simplifier
2002-08-27 wenzelm 2002-08-27 *** empty log message ***
2001-09-04 wenzelm 2001-09-04 renamed "antecedent" case to "rule_context";
2001-02-04 wenzelm 2001-02-04 HOL-NumberTheory: converted to new-style format and proper document setup;
2000-08-03 paulson 2000-08-03 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen