| Wed, 03 Mar 2010 00:33:02 +0100 |
wenzelm |
cleanup type translations;
|
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, 16 Dec 2008 21:31:55 -0800 |
huffman |
remove cvs Id tags
|
file |
diff |
annotate
|
| Fri, 20 Jun 2008 18:03:01 +0200 |
huffman |
added some lemmas; reorganized into sections; tuned proofs
|
file |
diff |
annotate
|
| Wed, 11 Jun 2008 15:41:08 +0200 |
wenzelm |
removed dead code;
|
file |
diff |
annotate
|
| Sun, 21 Oct 2007 16:27:42 +0200 |
wenzelm |
modernized specifications ('definition', 'axiomatization');
|
file |
diff |
annotate
|
| Sun, 21 Oct 2007 14:21:48 +0200 |
wenzelm |
modernized specifications ('definition', 'abbreviation', 'notation');
|
file |
diff |
annotate
|
| Thu, 03 Nov 2005 01:45:52 +0100 |
huffman |
changed order of arguments for constant behind If-then-else-fi syntax; added LAM patterns for TT, FF
|
file |
diff |
annotate
|
| Thu, 03 Nov 2005 00:12:29 +0100 |
huffman |
cleaned up; removed adm_tricks in favor of compactness theorems
|
file |
diff |
annotate
|
| Fri, 08 Jul 2005 02:42:42 +0200 |
huffman |
simplified proof of ifte_thms, removed ifte_simp
|
file |
diff |
annotate
|
| Fri, 01 Jul 2005 04:32:33 +0200 |
huffman |
defaultsort pcpo
|
file |
diff |
annotate
|
| Sat, 04 Jun 2005 02:11:20 +0200 |
huffman |
import Fix is unnecessary
|
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
|
| Fri, 01 Apr 2005 23:44:41 +0200 |
huffman |
convert to new-style theory
|
file |
diff |
annotate
|
| Mon, 21 Jun 2004 10:25:57 +0200 |
kleing |
Merged in license change from Isabelle2004
|
file |
diff |
annotate
|
| Sat, 03 Nov 2001 01:41:26 +0100 |
wenzelm |
GPLed;
|
file |
diff |
annotate
|
| Tue, 09 Jan 2001 15:32:27 +0100 |
nipkow |
*** empty log message ***
|
file |
diff |
annotate
|
| Fri, 10 Oct 1997 19:02:28 +0200 |
wenzelm |
fixed dots;
|
file |
diff |
annotate
|
| Sun, 25 May 1997 18:45:25 +0200 |
slotosch |
Eliminated ccc1. Moved ID,oo into Cfun.
|
file |
diff |
annotate
|
| Thu, 24 Apr 1997 17:51:27 +0200 |
mueller |
deleted definitions for blift and plift
|
file |
diff |
annotate
|
| Tue, 11 Mar 1997 14:21:10 +0100 |
wenzelm |
tr is (again) type abbrev;
|
file |
diff |
annotate
|
| Fri, 07 Mar 1997 15:28:22 +0100 |
wenzelm |
"bool lift" now syntax instead of type abbrev;
|
file |
diff |
annotate
|
| Tue, 04 Mar 1997 10:58:29 +0100 |
paulson |
Renamed constant "not" to "Not"
|
file |
diff |
annotate
|
| Mon, 17 Feb 1997 16:31:37 +0100 |
oheimb |
corrected type of plift
|
file |
diff |
annotate
|
| Mon, 17 Feb 1997 10:57:11 +0100 |
slotosch |
Changes of HOLCF from Oscar Slotosch:
|
file |
diff |
annotate
|