| Mon, 08 Aug 2011 09:52:09 -0700 |
huffman |
moved division ring stuff from Rings.thy to Fields.thy
|
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:23:24 +0900 |
Cezary Kaliszyk |
HOL/Import for HOLLight revival: Proper theory headers, update generation scripts to SVN version of HOL Light, add some constant maps and compatibility theorems
|
file |
diff |
annotate
|
| Sun, 16 Jan 2011 15:53:03 +0100 |
wenzelm |
tuned headers;
|
file |
diff |
annotate
|
| Sat, 28 Aug 2010 16:14:32 +0200 |
haftmann |
formerly unnamed infix equality now named HOL.eq
|
file |
diff |
annotate
|
| Fri, 27 Aug 2010 10:56:46 +0200 |
haftmann |
formerly unnamed infix conjunction and disjunction now named HOL.conj and HOL.disj
|
file |
diff |
annotate
|
| Thu, 26 Aug 2010 20:51:17 +0200 |
haftmann |
formerly unnamed infix impliciation now named HOL.implies
|
file |
diff |
annotate
|
| Thu, 01 Jul 2010 16:54:44 +0200 |
haftmann |
"prod" and "sum" replace "*" and "+" respectively
|
file |
diff |
annotate
|
| Thu, 10 Jun 2010 12:24:03 +0200 |
haftmann |
tuned quotes, antiquotations and whitespace
|
file |
diff |
annotate
|
| Fri, 19 Feb 2010 14:47:01 +0100 |
haftmann |
moved remaning class operations from Algebras.thy to Groups.thy
|
file |
diff |
annotate
|
| Thu, 28 Jan 2010 11:48:49 +0100 |
haftmann |
new theory Algebras.thy for generic algebraic structures
|
file |
diff |
annotate
|
| Thu, 03 Aug 2006 15:14:05 +0200 |
obua |
fixed generator
|
file |
diff |
annotate
|
| Tue, 01 Aug 2006 13:51:16 +0200 |
obua |
removed skip
|
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
|
| Tue, 07 Mar 2006 16:03:31 +0100 |
obua |
Added HOL-ZF to Isabelle.
|
file |
diff |
annotate
|
| Wed, 15 Feb 2006 23:57:06 +0100 |
obua |
fixed bugs, added caching
|
file |
diff |
annotate
|
| Mon, 26 Sep 2005 02:27:14 +0200 |
obua |
fixed disambiguation problem
|
file |
diff |
annotate
|
| Mon, 19 Sep 2005 22:35:39 +0200 |
obua |
maybe the last bug fix (sigh)?
|
file |
diff |
annotate
|
| Sat, 17 Sep 2005 11:49:29 +0200 |
obua |
1) mapped .. and == constants
|
file |
diff |
annotate
|
| Fri, 16 Sep 2005 21:02:15 +0200 |
obua |
fixed HOL-light/Isabelle syntax incompatability via more protect_xxx functions
|
file |
diff |
annotate
|
| Mon, 12 Sep 2005 15:52:00 +0200 |
obua |
Added HOLLight support to importer.
|
file |
diff |
annotate
|