src/HOL/Library/Parity.thy
2008-07-07 haftmann 2008-07-07 absolute imports of HOL/*.thy theories
2008-06-26 haftmann 2008-06-26 established Plain theory and image
2008-03-12 haftmann 2008-03-12 better improvement in instantiation target
2008-03-07 haftmann 2008-03-07 tuned
2008-01-09 nipkow 2008-01-09 added simp attributes/ proofs fixed
2007-12-18 haftmann 2007-12-18 switched from PreList to ATP_Linkup
2007-12-11 haftmann 2007-12-11 joined EvenOdd theory with Parity
2007-12-10 haftmann 2007-12-10 switched import from Main to PreList
2007-12-07 haftmann 2007-12-07 instantiation target rather than legacy instance
2007-11-29 haftmann 2007-11-29 instance command as rudimentary class target
2007-10-23 nipkow 2007-10-23 went back to >0
2007-10-21 nipkow 2007-10-21 Eliminated most of the neq0_conv occurrences. As a result, many theorems had to be rephrased with ~= 0 instead of > 0.
2007-07-02 chaieb 2007-07-02 Tuned proofs
2007-06-20 huffman 2007-06-20 remove simp attribute from of_nat_diff, for backward compatibility with zdiff_int
2007-06-20 huffman 2007-06-20 change simp rules for of_nat to work like int did previously (reorient of_nat_Suc, remove of_nat_mult [simp]); preserve original variable names in legacy int theorems
2007-06-11 huffman 2007-06-11 remove references to constant int::nat=>int
2007-03-20 haftmann 2007-03-20 explizit "type" superclass
2007-03-02 haftmann 2007-03-02 now using "class"
2006-11-17 wenzelm 2006-11-17 more robust syntax for definition/abbreviation/notation;
2006-11-09 wenzelm 2006-11-09 tuned;
2006-11-08 wenzelm 2006-11-08 moved theories Parity, GCD, Binomial to Library;