| Thu, 28 Feb 2013 12:24:24 +0100 |
wenzelm |
simplified imports;
|
file |
diff |
annotate
|
| Thu, 31 Jan 2013 11:31:30 +0100 |
hoelzl |
use order topology for extended reals
|
file |
diff |
annotate
|
| Fri, 19 Oct 2012 15:12:52 +0200 |
webertj |
Renamed {left,right}_distrib to distrib_{right,left}.
|
file |
diff |
annotate
|
| Fri, 12 Oct 2012 18:58:20 +0200 |
wenzelm |
discontinued obsolete typedef (open) syntax;
|
file |
diff |
annotate
|
| Sun, 25 Mar 2012 20:15:39 +0200 |
huffman |
merged fork with new numeral representation (see NEWS)
|
file |
diff |
annotate
|
| Tue, 20 Dec 2011 11:40:56 +0100 |
noschinl |
add simp rules for enat and ereal
|
file |
diff |
annotate
|
| Wed, 07 Dec 2011 10:50:30 +0100 |
huffman |
add cancellation simprocs for type enat
|
file |
diff |
annotate
|
| Thu, 17 Nov 2011 07:15:30 +0100 |
huffman |
remove redundant simp rules plus_enat_0
|
file |
diff |
annotate
|
| Mon, 12 Sep 2011 07:55:43 +0200 |
nipkow |
new fastforce replacing fastsimp - less confusing name
|
file |
diff |
annotate
|
| Tue, 02 Aug 2011 08:28:34 -0700 |
huffman |
Extended_Nat.thy: renamed iSuc to eSuc, standardized theorem names
|
file |
diff |
annotate
|
| Tue, 26 Jul 2011 13:50:03 +0200 |
hoelzl |
enat is a complete_linorder instance
|
file |
diff |
annotate
|
| Tue, 19 Jul 2011 14:38:48 +0200 |
hoelzl |
rename Fin to enat
|
file |
diff |
annotate
|
| Tue, 19 Jul 2011 14:38:29 +0200 |
hoelzl |
add ereal to typeclass infinity
|
file |
diff |
annotate
|
| Tue, 19 Jul 2011 14:37:49 +0200 |
hoelzl |
add nat => enat coercion
|
file |
diff |
annotate
|
| Tue, 19 Jul 2011 14:37:09 +0200 |
hoelzl |
Introduce infinity type class
|
file |
diff |
annotate
|
| Tue, 19 Jul 2011 14:35:44 +0200 |
hoelzl |
rename Nat_Infinity (inat) to Extended_Nat (enat)
|
file |
diff |
annotate
| base
|