| Fri, 18 Jan 2008 20:22:07 +0100 |
huffman |
change lemma admD to rule_format
|
file |
diff |
annotate
|
| Thu, 17 Jan 2008 21:56:33 +0100 |
huffman |
convert lemma lub_mono to rule_format
|
file |
diff |
annotate
|
| Thu, 17 Jan 2008 21:44:19 +0100 |
huffman |
rename lemma chain_mono3 -> chain_mono, chain_mono -> chain_mono_less
|
file |
diff |
annotate
|
| Thu, 17 Jan 2008 00:51:20 +0100 |
huffman |
change class axiom chfin to rule_format
|
file |
diff |
annotate
|
| Mon, 14 Jan 2008 03:49:53 +0100 |
huffman |
converted adm_all and adm_ball to rule_format; cleaned up
|
file |
diff |
annotate
|
| Thu, 10 Jan 2008 05:36:03 +0100 |
huffman |
Compactness subsection with some new lemmas
|
file |
diff |
annotate
|
| Thu, 03 Jan 2008 17:22:24 +0100 |
huffman |
remove legacy ML bindings
|
file |
diff |
annotate
|
| Thu, 03 Jan 2008 16:29:37 +0100 |
huffman |
new lemma adm_upward
|
file |
diff |
annotate
|
| Wed, 02 Jan 2008 18:57:40 +0100 |
huffman |
move lemmas from Cont.thy to Ffun.thy;
|
file |
diff |
annotate
|
| Sun, 21 Oct 2007 14:21:48 +0200 |
wenzelm |
modernized specifications ('definition', 'abbreviation', 'notation');
|
file |
diff |
annotate
|
| 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
|