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