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