Wed, 17 Nov 2010 08:14:56 +0100 | boehmes | use the const antiquotation for constants (this checks that the constant is declared, whereas the more general term antiquotation treats undeclared names as free variable) | 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 |
Wed, 12 May 2010 23:54:02 +0200 | boehmes | integrated SMT into the HOL image | file | diff | annotate |