| Thu, 01 Sep 2011 16:16:25 +0900 |
Cezary Kaliszyk |
HOL/Import: observe distinction between sets and predicates (where possible)
|
file |
diff |
annotate
|
| Sat, 16 Jul 2011 00:01:17 +0200 |
Cezary Kaliszyk |
HOL/Import: Fix errors with _mk_list
|
file |
diff |
annotate
|
| Wed, 13 Jul 2011 00:29:33 +0900 |
Cezary Kaliszyk |
Update files generated in HOL/Import/HOLLight
|
file |
diff |
annotate
|
| Mon, 01 Mar 2010 13:40:23 +0100 |
haftmann |
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
|
file |
diff |
annotate
|
| Thu, 28 Jan 2010 11:48:49 +0100 |
haftmann |
new theory Algebras.thy for generic algebraic structures
|
file |
diff |
annotate
|
| Fri, 10 Mar 2006 15:33:48 +0100 |
haftmann |
renamed HOL + - * etc. to HOL.plus HOL.minus HOL.times etc.
|
file |
diff |
annotate
|
| Fri, 17 Feb 2006 03:30:50 +0100 |
obua |
use monomorphic sequences / scanners
|
file |
diff |
annotate
|
| Wed, 19 Oct 2005 21:52:27 +0200 |
wenzelm |
isatool fixheaders;
|
file |
diff |
annotate
|
| Mon, 26 Sep 2005 16:10:19 +0200 |
obua |
Release HOL4 and HOLLight Importer.
|
file |
diff |
annotate
|
| Mon, 26 Sep 2005 02:27:14 +0200 |
obua |
fixed disambiguation problem
|
file |
diff |
annotate
|