| Wed, 02 Jan 2008 15:14:02 +0100 |
haftmann |
splitted class uminus from class minus
|
file |
diff |
annotate
|
| Fri, 07 Dec 2007 15:07:59 +0100 |
haftmann |
instantiation target rather than legacy instance
|
file |
diff |
annotate
|
| Thu, 29 Nov 2007 17:08:26 +0100 |
haftmann |
instance command as rudimentary class target
|
file |
diff |
annotate
|
| Thu, 08 Nov 2007 20:08:00 +0100 |
wenzelm |
eliminated illegal schematic variables in where/of;
|
file |
diff |
annotate
|
| Tue, 30 Oct 2007 08:45:54 +0100 |
haftmann |
continued localization
|
file |
diff |
annotate
|
| Thu, 25 Oct 2007 19:27:50 +0200 |
haftmann |
various localizations
|
file |
diff |
annotate
|
| Wed, 24 Oct 2007 07:19:53 +0200 |
haftmann |
dropped superfluous inlining rule
|
file |
diff |
annotate
|
| Wed, 26 Sep 2007 20:27:55 +0200 |
haftmann |
moved Finite_Set before Datatype
|
file |
diff |
annotate
|
| Sat, 01 Sep 2007 01:21:48 +0200 |
nipkow |
final(?) iteration of sgn saga.
|
file |
diff |
annotate
|
| Mon, 20 Aug 2007 19:52:52 +0200 |
huffman |
remove int_of_nat
|
file |
diff |
annotate
|
| Wed, 15 Aug 2007 12:52:56 +0200 |
paulson |
ATP blacklisting is now in theory data, attribute noatp
|
file |
diff |
annotate
|
| Thu, 09 Aug 2007 15:52:47 +0200 |
haftmann |
localized of_nat
|
file |
diff |
annotate
|
| Tue, 24 Jul 2007 15:20:48 +0200 |
haftmann |
dropped axclass
|
file |
diff |
annotate
|
| Fri, 20 Jul 2007 14:28:01 +0200 |
haftmann |
split class abs from class minus
|
file |
diff |
annotate
|
| Thu, 19 Jul 2007 21:47:37 +0200 |
haftmann |
moved set Nats to Nat.thy
|
file |
diff |
annotate
|
| 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
|