| 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
|
| Fri, 04 Jan 2008 00:01:02 +0100 |
huffman |
new instance proofs for classes finite_po, chfin, flat
|
file |
diff |
annotate
|
| Wed, 02 Jan 2008 18:57:40 +0100 |
huffman |
move lemmas from Cont.thy to Ffun.thy;
|
file |
diff |
annotate
|
| Thu, 20 Dec 2007 03:06:20 +0100 |
huffman |
move bottom-related stuff back into Pcpo.thy
|
file |
diff |
annotate
|
| Tue, 18 Dec 2007 22:18:31 +0100 |
huffman |
add class ppo of pointed partial orders;
|
file |
diff |
annotate
|
| Sun, 21 Oct 2007 16:27:42 +0200 |
wenzelm |
modernized specifications ('definition', 'axiomatization');
|
file |
diff |
annotate
|
| Sun, 21 Oct 2007 14:21:48 +0200 |
wenzelm |
modernized specifications ('definition', 'abbreviation', 'notation');
|
file |
diff |
annotate
|
| Thu, 31 May 2007 14:01:58 +0200 |
wenzelm |
moved HOLCF tools to canonical place;
|
file |
diff |
annotate
|
| Wed, 24 May 2006 01:47:25 +0200 |
huffman |
add theorem cfcomp_strict
|
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
|
| Sat, 05 Nov 2005 21:42:24 +0100 |
huffman |
add line breaks to Rep_CFun syntax
|
file |
diff |
annotate
|
| Fri, 04 Nov 2005 23:15:11 +0100 |
huffman |
moved adm_chfindom from Fix.thy to Cfun.thy
|
file |
diff |
annotate
|
| Fri, 04 Nov 2005 22:26:09 +0100 |
huffman |
add print translation: Abs_CFun f => LAM x. f x
|
file |
diff |
annotate
|
| Thu, 03 Nov 2005 01:28:22 +0100 |
huffman |
add translation for wildcard pattern
|
file |
diff |
annotate
|
| Thu, 03 Nov 2005 01:11:39 +0100 |
huffman |
change syntax for LAM to use expressions as patterns; define LAM pattern syntax for cpair, spair, sinl, sinr, up
|
file |
diff |
annotate
|
| Thu, 03 Nov 2005 00:57:35 +0100 |
huffman |
cleaned up; ch2ch_Rep_CFun is a simp rule
|
file |
diff |
annotate
|