src/HOLCF/ex/Domain_Proofs.thy
Fri, 29 Oct 2010 17:15:28 -0700 huffman renamed {Rep,Abs}_CFun to {Rep,Abs}_cfun
Tue, 19 Oct 2010 11:07:42 -0700 huffman replace 'in_defl' relation and '_ ::: _' syntax with 'defl_set' function
Tue, 19 Oct 2010 10:13:29 -0700 huffman eliminate constant 'coerce'; use 'prj oo emb' instead
Mon, 11 Oct 2010 08:32:09 -0700 huffman renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
Fri, 08 Oct 2010 07:39:50 -0700 huffman rename class 'sfp' to 'bifinite'
Wed, 06 Oct 2010 10:49:27 -0700 huffman major reorganization/simplification of HOLCF type classes:
Wed, 28 Apr 2010 12:07:52 +0200 wenzelm renamed command 'defaultsort' to 'default_sort';
Tue, 13 Apr 2010 11:04:27 -0700 huffman bring HOLCF/ex/Domain_Proofs.thy up to date
Mon, 01 Mar 2010 23:54:50 -0800 huffman need to explicitly include REP_convex
Thu, 19 Nov 2009 16:47:18 -0800 huffman fix definitions of copy combinators
Thu, 19 Nov 2009 10:26:53 -0800 huffman change example to use recursion with continuous function space
Thu, 19 Nov 2009 08:22:00 -0800 huffman change naming convention for deflation combinators
Thu, 19 Nov 2009 07:09:04 -0800 huffman avoid using csplit; define copy functions exactly like the current domain package
Wed, 18 Nov 2009 16:57:58 -0800 huffman remove one_typ and tr_typ; add abs/rep lemmas
Fri, 13 Nov 2009 15:31:20 -0800 huffman automate definition of representable domains from algebraic deflations
Tue, 10 Nov 2009 06:47:55 -0800 huffman HOLCF example: domain package proofs done manually
less more (0) tip