| Wed, 10 Nov 2010 17:56:08 -0800 |
huffman |
move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
|
file |
diff |
annotate
|
| Fri, 29 Oct 2010 17:15:28 -0700 |
huffman |
renamed {Rep,Abs}_CFun to {Rep,Abs}_cfun
|
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
|
| 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
|
| Thu, 07 Oct 2010 13:54:43 -0700 |
huffman |
move stuff from Algebraic.thy to Bifinite.thy and elsewhere
|
file |
diff |
annotate
|
| Tue, 05 Oct 2010 17:53:00 -0700 |
Brian Huffman |
add lemma finite_deflation_intro
|
file |
diff |
annotate
|
| Tue, 05 Oct 2010 17:32:02 -0700 |
Brian Huffman |
move lemmas to Deflation.thy
|
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
|
| Sun, 14 Mar 2010 19:48:33 -0700 |
huffman |
use headers consistently
|
file |
diff |
annotate
|
| Wed, 17 Feb 2010 08:19:46 -0800 |
huffman |
fix warnings about duplicate simp rules
|
file |
diff |
annotate
|
| Thu, 05 Nov 2009 11:36:30 -0800 |
huffman |
lemma deflation_strict
|
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
|
| Tue, 30 Dec 2008 11:10:01 +0100 |
ballarin |
Merged.
|
file |
diff |
annotate
|
| Tue, 16 Dec 2008 21:10:53 +0100 |
ballarin |
More porting to new locales.
|
file |
diff |
annotate
|
| Tue, 16 Dec 2008 21:31:55 -0800 |
huffman |
remove cvs Id tags
|
file |
diff |
annotate
|
| Thu, 16 Oct 2008 19:44:36 +0200 |
huffman |
rewrite more proofs in Isar style
|
file |
diff |
annotate
|
| Thu, 16 Oct 2008 17:19:47 +0200 |
ballarin |
More occurrences of 'includes' gone.
|
file |
diff |
annotate
|
| Fri, 25 Jul 2008 12:03:32 +0200 |
haftmann |
dropped locale (open)
|
file |
diff |
annotate
|
| Mon, 30 Jun 2008 21:52:17 +0200 |
huffman |
New theory of deflations and embedding-projection pairs
|
file |
diff |
annotate
|