| Thu, 13 Apr 2006 23:15:44 +0200 |
huffman |
add lemma less_UU_iff as default simp rule
|
file |
diff |
annotate
|
| Mon, 10 Oct 2005 04:12:31 +0200 |
huffman |
added notion of compactness; shortened proof of adm_disj; reorganized and cleaned up
|
file |
diff |
annotate
|
| Thu, 22 Sep 2005 19:06:34 +0200 |
huffman |
added theorem adm_ball
|
file |
diff |
annotate
|
| Thu, 07 Jul 2005 18:20:08 +0200 |
huffman |
use theorems ch2ch_cont, cont2contlubE
|
file |
diff |
annotate
|
| Fri, 01 Jul 2005 01:48:37 +0200 |
huffman |
cleaned up; added adm_less to adm_lemmas; added subsection headings
|
file |
diff |
annotate
|
| Sat, 25 Jun 2005 01:09:14 +0200 |
huffman |
cleaned up
|
file |
diff |
annotate
|
| Fri, 03 Jun 2005 23:15:16 +0200 |
huffman |
changed to work with new contlubE rule
|
file |
diff |
annotate
|
| Thu, 26 May 2005 00:30:24 +0200 |
huffman |
moved adm_chfindom from Adm.thy to Fix.thy, to remove dependence on Cfun
|
file |
diff |
annotate
|
| Wed, 25 May 2005 09:44:34 +0200 |
wenzelm |
removed LICENCE note -- everything is subject to Isabelle licence as
|
file |
diff |
annotate
|
| Tue, 24 May 2005 10:55:11 +0200 |
paulson |
cannot have files named adm.ML and Adm.ML on Macs, so deleted one and renamed the other
|
file |
diff |
annotate
|
| Tue, 24 May 2005 05:03:54 +0200 |
huffman |
Moved admissibility definitions and lemmas to a separate theory
|
file |
diff |
annotate
|