| Thu, 15 Jan 2009 14:33:38 -0800 |
huffman |
use match_tac instead of resolve_tac for continuity simproc
|
file |
diff |
annotate
|
| Wed, 14 Jan 2009 18:05:05 -0800 |
huffman |
add lemmas cont2monofunE, cont2cont_apply
|
file |
diff |
annotate
|
| Wed, 14 Jan 2009 17:11:29 -0800 |
huffman |
change to simpler, more extensible continuity simproc
|
file |
diff |
annotate
|
| Tue, 16 Dec 2008 21:31:55 -0800 |
huffman |
remove cvs Id tags
|
file |
diff |
annotate
|
| Tue, 01 Jul 2008 03:14:00 +0200 |
huffman |
remove unused lemmas ub2ub_monofun' and dir2dir_monofun
|
file |
diff |
annotate
|
| Tue, 01 Jul 2008 02:19:53 +0200 |
huffman |
replace lub (range Y) with (LUB i. Y i)
|
file |
diff |
annotate
|
| Thu, 27 Mar 2008 19:49:24 +0100 |
huffman |
declare cont_lemmas_ext as simp rules individually
|
file |
diff |
annotate
|
| Thu, 31 Jan 2008 21:48:14 +0100 |
huffman |
add lemma cpo_lubI
|
file |
diff |
annotate
|
| Thu, 31 Jan 2008 21:22:03 +0100 |
huffman |
new lemma cont_discrete_cpo
|
file |
diff |
annotate
|
| Wed, 16 Jan 2008 22:41:49 +0100 |
huffman |
change class axiom ax_flat to rule_format
|
file |
diff |
annotate
|
| Mon, 14 Jan 2008 03:54:31 +0100 |
huffman |
add lemma contI2
|
file |
diff |
annotate
|
| Thu, 03 Jan 2008 23:58:27 +0100 |
huffman |
generalized chfindom_monofun2cont
|
file |
diff |
annotate
|
| Wed, 02 Jan 2008 18:57:40 +0100 |
huffman |
move lemmas from Cont.thy to Ffun.thy;
|
file |
diff |
annotate
|
| Wed, 02 Jan 2008 18:28:15 +0100 |
huffman |
add lemma ub2ub_monofun'
|
file |
diff |
annotate
|
| Wed, 02 Jan 2008 17:26:19 +0100 |
huffman |
add lemma dir2dir_monofun
|
file |
diff |
annotate
|
| Sun, 21 Oct 2007 14:21:48 +0200 |
wenzelm |
modernized specifications ('definition', 'abbreviation', 'notation');
|
file |
diff |
annotate
|
| Sat, 05 Nov 2005 21:50:37 +0100 |
huffman |
renamed and added ch2ch, cont2cont, mono2mono theorems ending in _fun, _lambda, _LAM
|
file |
diff |
annotate
|
| Fri, 04 Nov 2005 22:27:40 +0100 |
huffman |
cleaned up
|
file |
diff |
annotate
|
| Tue, 11 Oct 2005 23:19:50 +0200 |
huffman |
cleaned up; renamed less_fun to expand_fun_less
|
file |
diff |
annotate
|
| Thu, 07 Jul 2005 18:19:20 +0200 |
huffman |
add lemmas ch2ch_cont and cont2contlubE
|
file |
diff |
annotate
|
| Fri, 01 Jul 2005 01:50:07 +0200 |
huffman |
cleaned up; reorganized and added section headings
|
file |
diff |
annotate
|
| Sat, 25 Jun 2005 01:04:01 +0200 |
huffman |
cleaned up proof of contlub_abstraction
|
file |
diff |
annotate
|
| Tue, 14 Jun 2005 04:05:15 +0200 |
huffman |
renamed theorem cont2cont_CF1L_rev2 to cont2cont_lambda
|
file |
diff |
annotate
|
| Fri, 03 Jun 2005 23:13:08 +0200 |
huffman |
renamed theorems monofun, contlub, cont to monofun_def, etc.; changed intro/elim rules for these predicates into more useful rule_format; removed all MF2 lemmas (Pcpo.thy has more general versions now); cleaned up many proofs.
|
file |
diff |
annotate
|
| Fri, 27 May 2005 01:12:15 +0200 |
huffman |
added lemmas monofun_lub_fun and cont_lub_fun
|
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
|
| Mon, 23 May 2005 23:01:27 +0200 |
huffman |
moved theorem cont2cont_CF1L_rev2 to Cont.thy
|
file |
diff |
annotate
|
| Thu, 10 Mar 2005 20:22:45 +0100 |
huffman |
fixed filename in header
|
file |
diff |
annotate
|
| Tue, 08 Mar 2005 00:00:49 +0100 |
huffman |
arranged for document generation, cleaned up some proofs
|
file |
diff |
annotate
|
| Fri, 04 Mar 2005 23:23:47 +0100 |
huffman |
fix headers
|
file |
diff |
annotate
|