| 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
|
| Wed, 06 May 2009 00:57:29 -0700 |
huffman |
replace cont2cont_apply with cont_apply; add new cont2cont lemmas
|
file |
diff |
annotate
|
| Wed, 14 Jan 2009 18:18:48 -0800 |
huffman |
minimize dependencies
|
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
|
| Thu, 11 Dec 2008 16:50:18 +0100 |
wenzelm |
pcpodef package: state two goals, instead of encoded conjunction;
|
file |
diff |
annotate
|
| Wed, 10 Dec 2008 17:15:26 -0800 |
huffman |
cleaned up some proofs in Cfun.thy
|
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, 19 Jun 2008 20:34:28 +0200 |
huffman |
add lemma cfcomp_LAM
|
file |
diff |
annotate
|
| Thu, 31 Jan 2008 21:23:14 +0100 |
huffman |
instances for class discrete_cpo
|
file |
diff |
annotate
|
| Fri, 18 Jan 2008 20:34:28 +0100 |
huffman |
add space to binder syntax
|
file |
diff |
annotate
|
| Thu, 17 Jan 2008 00:51:20 +0100 |
huffman |
change class axiom chfin to rule_format
|
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 18:25:20 +0100 |
huffman |
added lemmas lub_distribs
|
file |
diff |
annotate
|
| Thu, 10 Jan 2008 17:06:41 +0100 |
huffman |
declare ch2ch_LAM [simp]
|
file |
diff |
annotate
|