| 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
|