| Wed, 17 Nov 2010 08:47:58 -0800 |
huffman |
move strict function type into main HOLCF; instance cfun :: (predomain, domain) domain
|
file |
diff |
annotate
|
| Tue, 16 Nov 2010 11:50:05 -0800 |
huffman |
rename 'repdef' to 'domaindef'
|
file |
diff |
annotate
|
| Wed, 10 Nov 2010 18:30:17 -0800 |
huffman |
merge Representable.thy into Domain.thy
|
file |
diff |
annotate
|
| Wed, 10 Nov 2010 18:15:21 -0800 |
huffman |
move stuff from Domain.thy to Domain_Aux.thy
|
file |
diff |
annotate
|
| Wed, 27 Oct 2010 13:54:18 -0700 |
huffman |
rename lemmas *_defined_iff and *_strict_iff to *_bottom_iff
|
file |
diff |
annotate
|
| Tue, 19 Oct 2010 15:01:51 -0700 |
huffman |
rename domain_theorems.ML to domain_induction.ML; rename domain_extender.ML to domain.ML
|
file |
diff |
annotate
|
| Tue, 19 Oct 2010 14:28:14 -0700 |
huffman |
simplify some proofs; remove some unused lists of lemmas
|
file |
diff |
annotate
|
| Sat, 16 Oct 2010 16:22:42 -0700 |
huffman |
remove last few dependencies on domain_library.ML and delete it; temporarily disable emptiness check
|
file |
diff |
annotate
|
| Wed, 28 Apr 2010 12:07:52 +0200 |
wenzelm |
renamed command 'defaultsort' to 'default_sort';
|
file |
diff |
annotate
|
| Thu, 15 Apr 2010 18:21:05 -0700 |
huffman |
add rule deflation_ID to proof script for take + constructor rules
|
file |
diff |
annotate
|
| Mon, 08 Mar 2010 09:33:05 -0800 |
huffman |
move lemmas from Domain.thy to Domain_Aux.thy
|
file |
diff |
annotate
|
| Fri, 05 Mar 2010 14:50:37 -0800 |
huffman |
introduce notion of 'decisive' deflations; use them to simplify proof script for rule 'finites'
|
file |
diff |
annotate
|
| Tue, 02 Mar 2010 20:19:04 -0800 |
huffman |
remove dependency on domain_syntax.ML
|
file |
diff |
annotate
|
| Tue, 02 Mar 2010 20:04:17 -0800 |
huffman |
simplify add_axioms function; remove obsolete domain_syntax.ML
|
file |
diff |
annotate
|
| Tue, 02 Mar 2010 00:34:26 -0800 |
huffman |
domain package no longer generates copy functions; all proofs use take functions instead
|
file |
diff |
annotate
|
| Sat, 27 Feb 2010 08:30:11 -0800 |
huffman |
move proofs of casedist into domain_constructors.ML
|
file |
diff |
annotate
|
| Thu, 25 Feb 2010 13:16:28 -0800 |
huffman |
rewrite domain package code for selector functions
|
file |
diff |
annotate
|
| Wed, 24 Feb 2010 16:15:03 -0800 |
huffman |
reorganizing domain package code (in progress)
|
file |
diff |
annotate
|
| Thu, 11 Feb 2010 12:26:07 -0800 |
huffman |
change generated lemmas dist_eqs and dist_les to iff-style
|
file |
diff |
annotate
|
| Thu, 19 Nov 2009 16:48:40 -0800 |
huffman |
Domain.thy imports Representable.thy
|
file |
diff |
annotate
|
| Thu, 05 Nov 2009 11:47:00 -0800 |
huffman |
map functions for various types, with ep_pair/deflation/finite_deflation lemmas
|
file |
diff |
annotate
|
| Mon, 02 Nov 2009 17:29:34 -0800 |
huffman |
define cprod_fun using Pair instead of cpair
|
file |
diff |
annotate
|
| Tue, 21 Jul 2009 16:14:56 +0200 |
haftmann |
obey captialized directory names convention
|
file |
diff |
annotate
|
| Fri, 22 May 2009 10:34:22 -0700 |
huffman |
add combinators for building copy functions
|
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
|
| Fri, 10 Apr 2009 17:39:53 -0700 |
huffman |
domain package: simplify internal proofs of con_rews
|
file |
diff |
annotate
|
| Fri, 10 Apr 2009 11:35:21 -0700 |
huffman |
set up domain package in Domain.thy
|
file |
diff |
annotate
|
| Tue, 16 Dec 2008 21:31:55 -0800 |
huffman |
remove cvs Id tags
|
file |
diff |
annotate
|
| Thu, 03 Jan 2008 17:22:24 +0100 |
huffman |
remove legacy ML bindings
|
file |
diff |
annotate
|
| Wed, 13 Jun 2007 18:30:17 +0200 |
wenzelm |
tuned proofs: avoid implicit prems;
|
file |
diff |
annotate
|
| Thu, 31 May 2007 14:01:58 +0200 |
wenzelm |
moved HOLCF tools to canonical place;
|
file |
diff |
annotate
|
| Sun, 29 Jan 2006 19:24:56 +0100 |
wenzelm |
tuned proof;
|
file |
diff |
annotate
|
| Thu, 22 Dec 2005 00:29:22 +0100 |
wenzelm |
exh_casedist2: norm_hhf_eq;
|
file |
diff |
annotate
|
| Wed, 12 Oct 2005 03:01:30 +0200 |
huffman |
add ML bindings for compactness lemmas
|
file |
diff |
annotate
|
| Tue, 11 Oct 2005 23:47:29 +0200 |
huffman |
added compactness theorems in locale iso
|
file |
diff |
annotate
|
| Tue, 11 Oct 2005 23:27:49 +0200 |
huffman |
added several theorems in locale iso
|
file |
diff |
annotate
|
| Fri, 08 Jul 2005 02:41:35 +0200 |
huffman |
renamed upE1 to upE
|
file |
diff |
annotate
|
| Wed, 08 Jun 2005 01:41:20 +0200 |
huffman |
fixed renamed lemma
|
file |
diff |
annotate
|
| Sat, 04 Jun 2005 02:12:10 +0200 |
huffman |
fix imports
|
file |
diff |
annotate
|
| Sat, 04 Jun 2005 00:23:40 +0200 |
huffman |
add dependency on Fixrec.thy
|
file |
diff |
annotate
|
| Fri, 03 Jun 2005 23:36:17 +0200 |
huffman |
renamed defined lemmas
|
file |
diff |
annotate
|
| Tue, 31 May 2005 11:53:12 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Wed, 25 May 2005 09:44:34 +0200 |
wenzelm |
removed LICENCE note -- everything is subject to Isabelle licence as
|
file |
diff |
annotate
|
| Sat, 16 Apr 2005 00:16:44 +0200 |
huffman |
New file for theorems used by the domain package
|
file |
diff |
annotate
|