| Sat, 27 Nov 2010 14:09:03 -0800 |
huffman |
rename Pcpodef.thy to Cpodef.thy;
|
file |
diff |
annotate
|
| Sat, 27 Nov 2010 13:12:10 -0800 |
huffman |
renamed several HOLCF theorems (listed in NEWS)
|
file |
diff |
annotate
|
| Sat, 27 Nov 2010 12:55:12 -0800 |
huffman |
rename cpodef theorems: lub_foo -> is_lub_foo, thelub_foo -> lub_foo
|
file |
diff |
annotate
|
| Sat, 27 Nov 2010 12:26:18 -0800 |
huffman |
rename function 'strict' to 'seq', which is its name in Haskell
|
file |
diff |
annotate
|
| Wed, 10 Nov 2010 17:56:08 -0800 |
huffman |
move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
|
file |
diff |
annotate
|
| Wed, 03 Nov 2010 16:39:23 -0700 |
huffman |
remove some unnecessary lemmas; move monofun_LAM to Cfun.thy
|
file |
diff |
annotate
|
| Fri, 29 Oct 2010 17:15:28 -0700 |
huffman |
renamed {Rep,Abs}_CFun to {Rep,Abs}_cfun
|
file |
diff |
annotate
|
| Fri, 29 Oct 2010 16:51:40 -0700 |
huffman |
renamed lemma cont2cont_Rep_CFun to cont2cont_APP
|
file |
diff |
annotate
|
| Fri, 22 Oct 2010 15:47:43 -0700 |
huffman |
add lemma strict3
|
file |
diff |
annotate
|
| Fri, 22 Oct 2010 07:45:32 -0700 |
huffman |
make discrete_cpo a subclass of chfin; remove chfin instances for fun, cfun
|
file |
diff |
annotate
|
| Fri, 22 Oct 2010 06:58:45 -0700 |
huffman |
remove finite_po class
|
file |
diff |
annotate
|
| Wed, 20 Oct 2010 19:40:02 -0700 |
huffman |
introduce function strict :: 'a -> 'b -> 'b, which works like Haskell's seq; use strict instead of strictify in various definitions
|
file |
diff |
annotate
|
| Wed, 13 Oct 2010 10:56:42 -0700 |
huffman |
cleaned up Fun_Cpo.thy; deprecated a few theorem names
|
file |
diff |
annotate
|
| Tue, 12 Oct 2010 09:08:27 -0700 |
huffman |
move lemmas from Lift.thy to Cfun.thy
|
file |
diff |
annotate
|
| Tue, 12 Oct 2010 06:20:05 -0700 |
huffman |
remove unneeded lemmas from Fun_Cpo.thy
|
file |
diff |
annotate
|
| Tue, 12 Oct 2010 05:48:32 -0700 |
huffman |
remove unused lemmas
|
file |
diff |
annotate
|
| Tue, 12 Oct 2010 05:25:21 -0700 |
huffman |
remove unused lemmas cont_fst_snd_D1, cont_fst_snd_D2
|
file |
diff |
annotate
|
| Mon, 11 Oct 2010 21:35:31 -0700 |
huffman |
new theorem names: fun_below_iff, fun_belowI, cfun_eq_iff, cfun_eqI, cfun_below_iff, cfun_belowI
|
file |
diff |
annotate
|
| Mon, 11 Oct 2010 16:24:44 -0700 |
huffman |
rename Ffun.thy to Fun_Cpo.thy
|
file |
diff |
annotate
|
| Thu, 07 Oct 2010 13:54:43 -0700 |
huffman |
move stuff from Algebraic.thy to Bifinite.thy and elsewhere
|
file |
diff |
annotate
|
| Thu, 30 Sep 2010 18:46:19 -0700 |
huffman |
rename cont2cont_split to cont2cont_prod_case; add lemmas prod_contI, prod_cont_iff; simplify some proofs
|
file |
diff |
annotate
|
| Mon, 13 Sep 2010 11:13:15 +0200 |
nipkow |
renamed lemmas: ext_iff -> fun_eq_iff, set_ext_iff -> set_eq_iff, set_ext -> set_eqI
|
file |
diff |
annotate
|
| Tue, 07 Sep 2010 12:04:18 +0200 |
nipkow |
renamed expand_*_eq in HOLCF as well
|
file |
diff |
annotate
|
| Sat, 04 Sep 2010 08:32:19 -0700 |
huffman |
add lemma cont2cont_Let_simple
|
file |
diff |
annotate
|
| Sat, 22 May 2010 13:40:15 -0700 |
huffman |
add beta_cfun simproc, which uses cont2cont rules
|
file |
diff |
annotate
|
| Sat, 22 May 2010 10:02:07 -0700 |
huffman |
remove cont2cont simproc; instead declare cont2cont rules as simp rules
|
file |
diff |
annotate
|
| Wed, 28 Apr 2010 12:07:52 +0200 |
wenzelm |
renamed command 'defaultsort' to 'default_sort';
|
file |
diff |
annotate
|
| Tue, 23 Mar 2010 10:07:39 -0700 |
huffman |
remove continuous let-binding function CLet; add cont2cont rule ordinary Let
|
file |
diff |
annotate
|
| Mon, 22 Mar 2010 20:54:52 -0700 |
huffman |
remove contlub predicate
|
file |
diff |
annotate
|
| Sun, 14 Mar 2010 19:48:33 -0700 |
huffman |
use headers consistently
|
file |
diff |
annotate
|
| Sun, 07 Mar 2010 16:12:01 -0800 |
huffman |
add simp rule LAM_strict
|
file |
diff |
annotate
|
| Wed, 03 Mar 2010 16:43:55 +0100 |
wenzelm |
merged, resolving some basic conflicts;
|
file |
diff |
annotate
|
| Tue, 02 Mar 2010 17:21:10 -0800 |
huffman |
proper names for types cfun, sprod, ssum
|
file |
diff |
annotate
|
| Tue, 02 Mar 2010 23:59:54 +0100 |
wenzelm |
proper (type_)notation;
|
file |
diff |
annotate
|
| Wed, 17 Feb 2010 08:19:46 -0800 |
huffman |
fix warnings about duplicate simp rules
|
file |
diff |
annotate
|
| Thu, 11 Feb 2010 23:00:22 +0100 |
wenzelm |
modernized translations;
|
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
|
| 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
|