2007-08-15 paulson 2007-08-15 ATP blacklisting is now in theory data, attribute noatp
2007-08-09 haftmann 2007-08-09 localized of_nat
2007-07-24 haftmann 2007-07-24 dropped axclass
2007-07-20 haftmann 2007-07-20 split class abs from class minus
2007-07-19 haftmann 2007-07-19 moved set Nats to Nat.thy
2007-07-10 haftmann 2007-07-10 moved finite lemmas to Finite_Set.thy
2007-06-23 nipkow 2007-06-23 tuned and renamed group_eq_simps and ring_eq_simps
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-17 nipkow 2007-06-17 renamed vars in zle_trans for compatibility
2007-06-13 huffman 2007-06-13 clean up instance proofs; reorganize section headings
2007-06-13 huffman 2007-06-13 removed constant int :: nat => int; int is now an abbreviation for of_nat :: nat => int
2007-06-11 huffman 2007-06-11 simplify int proofs
2007-06-11 huffman 2007-06-11 modify proofs to avoid referring to int::nat=>int
2007-06-11 huffman 2007-06-11 add abbreviation int_of_nat for of_nat::nat=>int; add int_of_nat versions of all lemmas about int::nat=>int; move int lemmas into their own section, preparing to remove
2007-06-09 huffman 2007-06-09 remove dependencies of proofs on constant int::nat=>int, preparing to remove it
2007-06-06 huffman 2007-06-06 add axclass semiring_char_0 for types where of_nat is injective
2007-06-06 huffman 2007-06-06 generalize of_nat and related constants to class semiring_1
2007-05-31 wenzelm 2007-05-31 moved Integ files to canonical place;