| Wed, 02 Jan 2008 15:14:22 +0100 |
haftmann |
absolute import
|
file |
diff |
annotate
|
| Wed, 20 Jun 2007 19:49:14 +0200 |
huffman |
avoid using implicit prems in assumption
|
file |
diff |
annotate
|
| Wed, 06 Jun 2007 19:12:40 +0200 |
nipkow |
hide filter
|
file |
diff |
annotate
|
| Thu, 14 Dec 2006 22:08:35 +0100 |
huffman |
declare insert_iff [simp]
|
file |
diff |
annotate
|
| Thu, 14 Dec 2006 19:29:48 +0100 |
huffman |
add lemmas singleton and insert_iff
|
file |
diff |
annotate
|
| Sun, 01 Oct 2006 18:29:26 +0200 |
wenzelm |
moved theory Infinite_Set to Library;
|
file |
diff |
annotate
|
| Tue, 04 Jul 2006 14:47:01 +0200 |
ballarin |
Method intro_locales replaced by intro_locales and unfold_locales.
|
file |
diff |
annotate
|
| Tue, 20 Jun 2006 15:53:44 +0200 |
ballarin |
Restructured locales with predicates: import is now an interpretation.
|
file |
diff |
annotate
|
| Mon, 12 Sep 2005 23:14:41 +0200 |
huffman |
added theorem attributes transfer_intro, transfer_unfold, transfer_refold; simplified some proofs; some rearranging
|
file |
diff |
annotate
|
| Tue, 06 Sep 2005 19:22:31 +0200 |
huffman |
reimplement Filter.thy with locales
|
file |
diff |
annotate
|
| Wed, 18 Aug 2004 11:09:40 +0200 |
nipkow |
import -> imports
|
file |
diff |
annotate
|
| Mon, 16 Aug 2004 14:22:27 +0200 |
nipkow |
New theory header syntax.
|
file |
diff |
annotate
|
| Sat, 31 Jul 2004 20:54:23 +0200 |
paulson |
conversion of Hyperreal/{Fact,Filter} to Isar scripts
|
file |
diff |
annotate
|
| Sat, 30 Dec 2000 22:03:46 +0100 |
paulson |
separation of HOL-Hyperreal from HOL-Real
|
file |
diff |
annotate
|