| Wed, 17 Nov 2010 16:13:33 -0800 |
huffman |
declare adm_chfin [simp]
|
file |
diff |
annotate
|
| Wed, 10 Nov 2010 14:20:47 -0800 |
huffman |
add lemmas lub_below, below_lub; simplify some proofs; remove some unused lemmas
|
file |
diff |
annotate
|
| Wed, 03 Nov 2010 17:22:25 -0700 |
huffman |
simplify some proofs
|
file |
diff |
annotate
|
| Wed, 03 Nov 2010 15:31:24 -0700 |
huffman |
move a few admissibility lemmas into FOCUS/Stream_adm.thy
|
file |
diff |
annotate
|
| Tue, 12 Oct 2010 07:46:44 -0700 |
huffman |
cleaned up Adm.thy
|
file |
diff |
annotate
|
| Mon, 04 Oct 2010 06:58:37 -0700 |
huffman |
new lemmas about lub
|
file |
diff |
annotate
|
| Wed, 28 Apr 2010 12:07:52 +0200 |
wenzelm |
renamed command 'defaultsort' to 'default_sort';
|
file |
diff |
annotate
|
| Fri, 08 May 2009 16:19:51 -0700 |
huffman |
rename constant sq_le to below; rename class sq_ord to below; less->below in many lemma names
|
file |
diff |
annotate
|
| Tue, 16 Dec 2008 21:31:55 -0800 |
huffman |
remove cvs Id tags
|
file |
diff |
annotate
|
| Tue, 01 Jul 2008 06:56:37 +0200 |
huffman |
range_composition no longer in simp set
|
file |
diff |
annotate
|
| Tue, 01 Jul 2008 02:19:53 +0200 |
huffman |
replace lub (range Y) with (LUB i. Y i)
|
file |
diff |
annotate
|
| Fri, 20 Jun 2008 17:43:16 +0200 |
huffman |
tweak lemmas adm_all and adm_ball
|
file |
diff |
annotate
|
| Thu, 12 Jun 2008 22:14:07 +0200 |
huffman |
remove unnecessary import of Ffun;
|
file |
diff |
annotate
|
| Wed, 07 May 2008 10:59:51 +0200 |
berghofe |
Adm now imports Ffun rather than Cont, because SetPcpo, which imports Adm,
|
file |
diff |
annotate
|
| 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
|