src/HOL/IntDef.thy
Tue, 24 Jul 2007 15:20:48 +0200 haftmann dropped axclass
Fri, 20 Jul 2007 14:28:01 +0200 haftmann split class abs from class minus
Thu, 19 Jul 2007 21:47:37 +0200 haftmann moved set Nats to Nat.thy
Tue, 10 Jul 2007 17:30:43 +0200 haftmann moved finite lemmas to Finite_Set.thy
Sat, 23 Jun 2007 19:33:22 +0200 nipkow tuned and renamed group_eq_simps and ring_eq_simps
Wed, 20 Jun 2007 17:28:55 +0200 huffman remove simp attribute from of_nat_diff, for backward compatibility with zdiff_int
Wed, 20 Jun 2007 05:18:39 +0200 huffman 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
Sun, 17 Jun 2007 08:56:13 +0200 nipkow renamed vars in zle_trans for compatibility
Wed, 13 Jun 2007 16:43:02 +0200 huffman clean up instance proofs; reorganize section headings
Wed, 13 Jun 2007 03:31:11 +0200 huffman removed constant int :: nat => int;
Mon, 11 Jun 2007 06:14:32 +0200 huffman simplify int proofs
Mon, 11 Jun 2007 05:20:05 +0200 huffman modify proofs to avoid referring to int::nat=>int
Mon, 11 Jun 2007 00:53:18 +0200 huffman add abbreviation int_of_nat for of_nat::nat=>int;
Sat, 09 Jun 2007 02:38:51 +0200 huffman remove dependencies of proofs on constant int::nat=>int, preparing to remove it
Wed, 06 Jun 2007 20:49:04 +0200 huffman add axclass semiring_char_0 for types where of_nat is injective
Wed, 06 Jun 2007 17:00:09 +0200 huffman generalize of_nat and related constants to class semiring_1
Thu, 31 May 2007 18:16:52 +0200 wenzelm moved Integ files to canonical place;
less more (0) tip