| Thu, 09 Jun 2011 23:12:02 +0200 |
wenzelm |
renamed Drule.instantiate to Drule.instantiate_normalize to emphasize its meaning as opposed to plain Thm.instantiate;
|
file |
diff |
annotate
|
| Wed, 03 Nov 2010 10:48:55 +0100 |
wenzelm |
replaced ancient sys_error by raise Fail, assuming that the latter is not handled specifically by the environment;
|
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, 19 Aug 2010 16:08:59 +0200 |
haftmann |
tuned quotes
|
file |
diff |
annotate
|
| Thu, 19 Aug 2010 11:02:14 +0200 |
haftmann |
use antiquotations for remaining unqualified constants in HOL
|
file |
diff |
annotate
|
| Thu, 08 Jul 2010 16:19:24 +0200 |
haftmann |
tuned titles
|
file |
diff |
annotate
|
| Tue, 25 May 2010 22:21:31 +0200 |
wenzelm |
moved ML files where they are actually used;
|
file |
diff |
annotate
| base
|