| Wed, 10 Nov 2010 11:42:35 -0800 |
huffman |
rename class 'bifinite' to 'domain'
|
file |
diff |
annotate
|
| Wed, 10 Nov 2010 08:18:32 -0800 |
huffman |
add class liftdomain, for bifinite domains where DEFL('a u) = u_defl('a)
|
file |
diff |
annotate
|
| Wed, 10 Nov 2010 06:02:37 -0800 |
huffman |
instance prod :: (predomain, predomain) predomain
|
file |
diff |
annotate
|
| Tue, 09 Nov 2010 16:37:13 -0800 |
huffman |
add 'predomain' class: unpointed version of bifinite
|
file |
diff |
annotate
|
| Mon, 08 Nov 2010 15:13:45 -0800 |
huffman |
implement defl_of_typ using Pattern.rewrite_term instead of DeflData theory data
|
file |
diff |
annotate
|
| Wed, 27 Oct 2010 11:10:36 -0700 |
huffman |
make domain package work with non-cpo argument types
|
file |
diff |
annotate
|
| Tue, 26 Oct 2010 14:19:59 -0700 |
huffman |
use Named_Thms instead of Theory_Data for some domain package theorems
|
file |
diff |
annotate
|
| Tue, 19 Oct 2010 11:07:42 -0700 |
huffman |
replace 'in_defl' relation and '_ ::: _' syntax with 'defl_set' function
|
file |
diff |
annotate
|
| Tue, 19 Oct 2010 10:13:29 -0700 |
huffman |
eliminate constant 'coerce'; use 'prj oo emb' instead
|
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 08:32:09 -0700 |
huffman |
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
|
file |
diff |
annotate
|
| Sat, 09 Oct 2010 07:24:49 -0700 |
huffman |
move all bifinite class instances to Bifinite.thy
|
file |
diff |
annotate
|
| Fri, 08 Oct 2010 07:39:50 -0700 |
huffman |
rename class 'sfp' to 'bifinite'
|
file |
diff |
annotate
|
| Wed, 06 Oct 2010 10:49:27 -0700 |
huffman |
major reorganization/simplification of HOLCF type classes:
|
file |
diff |
annotate
|
| Mon, 12 Jul 2010 11:39:27 +0200 |
haftmann |
avoid explicit mandatory prefix markers when prefixes are mandatory implicitly
|
file |
diff |
annotate
|
| Thu, 01 Jul 2010 16:54:44 +0200 |
haftmann |
"prod" and "sum" replace "*" and "+" respectively
|
file |
diff |
annotate
|
| Wed, 28 Apr 2010 12:07:52 +0200 |
wenzelm |
renamed command 'defaultsort' to 'default_sort';
|
file |
diff |
annotate
|
| Mon, 22 Mar 2010 13:27:35 -0700 |
huffman |
fix LaTeX overfull hbox warnings in HOLCF document
|
file |
diff |
annotate
|
| Mon, 22 Mar 2010 12:52:51 -0700 |
huffman |
remove LaTeX hyperref warnings by avoiding antiquotations within section headings
|
file |
diff |
annotate
|
| Mon, 08 Mar 2010 08:12:48 -0800 |
huffman |
move take-proofs stuff into new theory Domain_Aux.thy
|
file |
diff |
annotate
|
| Fri, 05 Mar 2010 14:05:25 -0800 |
huffman |
add comment
|
file |
diff |
annotate
|
| Fri, 05 Mar 2010 13:56:04 -0800 |
huffman |
move take_proofs-related stuff to a new section
|
file |
diff |
annotate
|
| Wed, 03 Mar 2010 10:40:40 -0800 |
huffman |
merged
|
file |
diff |
annotate
|
| Wed, 03 Mar 2010 07:36:31 -0800 |
huffman |
uniformly use variable names m and n in take-related lemmas; use export_without_context where appropriate
|
file |
diff |
annotate
|
| Wed, 03 Mar 2010 16:43:55 +0100 |
wenzelm |
merged, resolving some basic conflicts;
|
file |
diff |
annotate
|
| Tue, 02 Mar 2010 18:16:28 -0800 |
huffman |
fixrec and repdef modules import holcf_library
|
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 13:50:23 -0800 |
huffman |
move take-related definitions and proofs to new module; simplify map_of_typ functions
|
file |
diff |
annotate
|
| Mon, 01 Mar 2010 16:58:16 -0800 |
huffman |
generate take_take rules
|
file |
diff |
annotate
|
| Mon, 01 Mar 2010 16:36:25 -0800 |
huffman |
add function define_take_functions
|
file |
diff |
annotate
|
| Sun, 28 Feb 2010 19:39:50 -0800 |
huffman |
domain_isomorphism package proves deflation rules for map functions
|
file |
diff |
annotate
|
| Sun, 28 Feb 2010 18:33:57 -0800 |
huffman |
store deflation thms for map functions in theory data
|
file |
diff |
annotate
|
| Sun, 28 Feb 2010 15:30:44 -0800 |
huffman |
move common functions into new file holcf_library.ML
|
file |
diff |
annotate
|
| Sun, 28 Feb 2010 14:55:42 -0800 |
huffman |
move some powerdomain stuff into a new file
|
file |
diff |
annotate
|
| Wed, 03 Mar 2010 00:33:02 +0100 |
wenzelm |
cleanup type translations;
|
file |
diff |
annotate
|
| Thu, 19 Nov 2009 22:25:11 -0800 |
huffman |
store map_ID thms in theory data; automate proofs of reach lemmas
|
file |
diff |
annotate
|
| Thu, 19 Nov 2009 12:38:02 -0800 |
huffman |
set up domain_isomorphism package in Representable.thy
|
file |
diff |
annotate
|
| Thu, 19 Nov 2009 10:25:17 -0800 |
huffman |
add lemma isodefl_cprod
|
file |
diff |
annotate
|
| Thu, 19 Nov 2009 08:22:00 -0800 |
huffman |
change naming convention for deflation combinators
|
file |
diff |
annotate
|
| Wed, 18 Nov 2009 16:57:58 -0800 |
huffman |
remove one_typ and tr_typ; add abs/rep lemmas
|
file |
diff |
annotate
|
| Fri, 13 Nov 2009 15:31:20 -0800 |
huffman |
automate definition of representable domains from algebraic deflations
|
file |
diff |
annotate
|
| Tue, 10 Nov 2009 06:30:08 -0800 |
huffman |
add title/author block
|
file |
diff |
annotate
|
| Tue, 10 Nov 2009 06:22:29 -0800 |
huffman |
theory of representable cpos
|
file |
diff |
annotate
|