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