You can subscribe to this list here.
2003 
_{Jan}

_{Feb}

_{Mar}

_{Apr}

_{May}

_{Jun}

_{Jul}

_{Aug}
(12) 
_{Sep}
(8) 
_{Oct}
(20) 
_{Nov}
(21) 
_{Dec}
(3) 

2004 
_{Jan}
(16) 
_{Feb}
(11) 
_{Mar}
(26) 
_{Apr}
(15) 
_{May}
(17) 
_{Jun}
(10) 
_{Jul}
(3) 
_{Aug}
(4) 
_{Sep}
(11) 
_{Oct}

_{Nov}
(11) 
_{Dec}
(8) 
2005 
_{Jan}
(16) 
_{Feb}
(18) 
_{Mar}
(22) 
_{Apr}
(23) 
_{May}
(17) 
_{Jun}
(22) 
_{Jul}
(10) 
_{Aug}
(9) 
_{Sep}
(13) 
_{Oct}
(26) 
_{Nov}
(26) 
_{Dec}
(31) 
2006 
_{Jan}
(29) 
_{Feb}
(35) 
_{Mar}
(20) 
_{Apr}
(23) 
_{May}
(35) 
_{Jun}
(17) 
_{Jul}
(18) 
_{Aug}
(11) 
_{Sep}
(18) 
_{Oct}
(12) 
_{Nov}
(16) 
_{Dec}
(27) 
2007 
_{Jan}
(27) 
_{Feb}
(22) 
_{Mar}
(15) 
_{Apr}
(38) 
_{May}
(26) 
_{Jun}
(24) 
_{Jul}
(8) 
_{Aug}
(20) 
_{Sep}
(21) 
_{Oct}
(23) 
_{Nov}
(20) 
_{Dec}
(24) 
2008 
_{Jan}
(16) 
_{Feb}
(19) 
_{Mar}
(24) 
_{Apr}
(54) 
_{May}
(24) 
_{Jun}
(21) 
_{Jul}
(20) 
_{Aug}
(12) 
_{Sep}
(19) 
_{Oct}
(28) 
_{Nov}
(26) 
_{Dec}
(34) 
2009 
_{Jan}
(22) 
_{Feb}
(15) 
_{Mar}
(20) 
_{Apr}
(33) 
_{May}
(27) 
_{Jun}
(30) 
_{Jul}
(23) 
_{Aug}
(13) 
_{Sep}
(21) 
_{Oct}
(19) 
_{Nov}
(29) 
_{Dec}
(22) 
2010 
_{Jan}
(36) 
_{Feb}
(30) 
_{Mar}
(58) 
_{Apr}
(38) 
_{May}
(36) 
_{Jun}
(35) 
_{Jul}
(22) 
_{Aug}
(8) 
_{Sep}
(40) 
_{Oct}
(27) 
_{Nov}
(29) 
_{Dec}
(23) 
2011 
_{Jan}
(31) 
_{Feb}
(39) 
_{Mar}
(30) 
_{Apr}
(49) 
_{May}
(38) 
_{Jun}
(27) 
_{Jul}
(11) 
_{Aug}
(13) 
_{Sep}
(20) 
_{Oct}
(28) 
_{Nov}
(23) 
_{Dec}
(18) 
2012 
_{Jan}
(36) 
_{Feb}
(39) 
_{Mar}
(61) 
_{Apr}
(71) 
_{May}
(188) 
_{Jun}
(117) 
_{Jul}
(132) 
_{Aug}
(153) 
_{Sep}
(32) 
_{Oct}
(44) 
_{Nov}
(64) 
_{Dec}
(56) 
2013 
_{Jan}
(85) 
_{Feb}
(36) 
_{Mar}
(44) 
_{Apr}
(130) 
_{May}
(47) 
_{Jun}
(33) 
_{Jul}
(34) 
_{Aug}
(25) 
_{Sep}
(20) 
_{Oct}
(49) 
_{Nov}
(20) 
_{Dec}
(39) 
2014 
_{Jan}
(38) 
_{Feb}
(61) 
_{Mar}
(83) 
_{Apr}
(56) 
_{May}
(42) 
_{Jun}
(37) 
_{Jul}
(24) 
_{Aug}
(16) 
_{Sep}
(28) 
_{Oct}
(33) 
_{Nov}
(21) 
_{Dec}
(22) 
2015 
_{Jan}
(12) 
_{Feb}
(43) 
_{Mar}
(46) 
_{Apr}
(36) 
_{May}
(57) 
_{Jun}
(29) 
_{Jul}
(19) 
_{Aug}
(21) 
_{Sep}
(17) 
_{Oct}
(20) 
_{Nov}
(77) 
_{Dec}
(30) 
2016 
_{Jan}
(20) 
_{Feb}
(39) 
_{Mar}
(53) 
_{Apr}
(32) 
_{May}
(47) 
_{Jun}
(53) 
_{Jul}
(30) 
_{Aug}
(17) 
_{Sep}
(17) 
_{Oct}
(56) 
_{Nov}
(14) 
_{Dec}
(23) 
2017 
_{Jan}
(87) 
_{Feb}
(39) 
_{Mar}
(49) 
_{Apr}
(83) 
_{May}
(65) 
_{Jun}
(25) 
_{Jul}
(65) 
_{Aug}
(19) 
_{Sep}

_{Oct}

_{Nov}

_{Dec}

S  M  T  W  T  F  S 


1

2
(4) 
3
(1) 
4

5

6

7

8

9

10
(3) 
11
(1) 
12

13

14

15

16
(1) 
17

18

19

20

21

22

23
(1) 
24

25

26

27
(1) 
28
(1) 
29
(1) 
30
(12) 
31
(1) 



From: Michael Norrish <Michael.Norrish@ni...>  20070103 04:17:36

We're pleased to announce that the latest version of HOL is now available for download from http://hol.sourceforge.net in both source and Windows selfextracting installer formats. Release notes below. Regards, Michael.  Notes on HOL 4, Kananaskis4 release New features: * There is a new unambiguous notation for set comprehensions that allows one to specify exactly what variables can "vary" to generate the set. For example, the current notation interprets { x + y  x < y } as the set that takes all pairs of numbers such that the first component is less than the other, and then sums them (generating the set of all nonzero numbers). The new notation allows one to specify that only the x should vary by writing { x + y  x  x < y } This denotes the set of numbers from y up to but not including 2 * y. To express the first set in the new notation, one would write { x + y  x,y  x < y } The parser accepts both notations. The prettyprinter prefers the old notation unless it can not express the set being printed. Further details are in the Description. Thanks to John Harrison for discussion leading to the adoption of this syntax. * The syntax of string and character literals is now the same as that accepted by SML. This means that escapes such as \n (for the linefeed character) and \^E (for ASCII character no. 5) can be used inside string and character literals. The SML syntax which allows strings to be broken over newlines by using backslashes is also supported. This means that one can write ``mystring = "the quick brown fox jumps over \ \the lazy dog"`` and have the actual string value generated exclude the whitespace appearing between the backslashes. * It is possible to include both ^ (caret) and ` backtick characters inside quotations. Usually these characters have special meaning inside quotations: caret is used to introduce an antiquotation, and the backtick is used to end a quotation (singly or doubly, depending on the sort of quotation). The caret character can be used as is if a sequence of them is followed by whitespace. Otherwise, it needs to be "escaped" by preceding it with another caret character. Similarly, the backquote character can be written by escaping it with a caret. For example, writing ``s1 ^ s2`` will result in the string s1 ^ s2 being passed to the HOL parser. This string will then be treated in the standard fashion. E.g., if ^ is an infix, a function application with it as the head operator will be created. If one wrote ``s1 ^^ s2`` this would also pass through unchanged. However, if one wrote ``s1 ^s2`` this would be taken as an antiquotation of SML variable s2. One should write ``s1 ^^s2`` to get the single caret passed to the underlying lexer. Note that the backquote character always needs to be escaped by a caret, and that caretescapes need to be applied even within string literals and comments that occur inside quotations. * The XEmacs editor is now supported, in addition to Emacs, by the tools/hol98mode.el file of Emacs extensions. * Case expressions may now include literals as patterns, in addition to constructor expressions as in the past. These literals may be for example of types num, char, or string; or they may be of any other type as well, even function types. Literals need not be constants, but they must not contain any free variables. case n of 0 > "none"  1 > "one"  2 > "two"  _ > "many" Patterns in case expressions are similar to the patterns used in the definition of recursive functions by Define. Thus they may be deeply nested within larger patterns. As before, in case of overlapping patterns, the earliest listed pattern is matched. If the set of patterns specified is sparse, there may be new rows generated automatically to fill it out, and possibly some new or renamed variables or the ARB constant to properly represent the case expression.  ``case a of (1, y, z) > y + z  (x, 2, z) > x  z  (x, y, 3) > x * y``; > val it = ``case a of (1,2,3) > 2 + 3  (1,2,z) > 2 + z  (1,y,3) > y + 3  (1,y,z) > y + z  (x,2,3) > x  3  (x,2,z') > x  z'  (x,y',3) > x * y'  (x,y',z') > ARB`` : term A complex pattern with several components may include both literals and constructor expressions as subpatterns. However, a set of patterns specified in a case expression may not have both literals and constructor expressions as alternatives to each other, except insofar as a pattern may be both a literal and a (0ary) constructor, such as the literal 0. See the Description for more information and examples of case expressions. * Inductive definitions are now made with respect to a varying "monoset": a list of theorems specifying that boolean operators are monotone in their arguments. These are used to justify recursions that may occur underneath new operators that users introduce. Initially, this set includes results for the standard boolean operators (such as existential quantification and conjunction), and is augmented as later theories are loaded. For example, the constant EVERY in the theory of lists, has a monotonicity result  (!x:'a. P x ==> Q x) ==> (EVERY P l ==> EVERY Q l) and this is incorporated into the global monoset when the theory of lists is loaded. This then allows the easy definition of relations that recurse under EVERY, as in this rule !x. EVERY newrel (somelist_of x) ==> newrel x Theorems can be declared as monotonicity results using the export_mono function. See the Description for the exact form that monotonicity theorems must take. * Types that are instances of abbreviation patterns (made with type_abbrev) now print in abbreviated form by default. For example, if one writes type_abbrev("set", ``:'a > bool``); Then, as before, one can write ``:num set`` and have this understood by the type parser. Now, in addition, when types are printed, this is reversed, so that the following works:  type_of ``(UNION)``; > val it = ``:'a set > 'a set > 'a set`` : hol_type Unfortunately, with this particular example, one also gets  type_of ``(/\)``; > val it = ``:bool > bool set`` : hol_type which is more confusing than it is illuminating. For this reason, it is possible to turn abbreviation printing off globally (using a trace variable, print_tyabbrevs), or on an abbreviationbyabbreviation basis. The latter is done with the function disable_tyabbrev_printing : string > unit Calls to this function are made in the pred_set and bag theories so that those theories' abbreviations (set, bag and multiset) are not printed. * There is a new polymorphic type, ``:'a itself`` containing just one value for all possible instantiations of ``:'a``. This value is supported by special syntax, and can be written (:tyname) This type provides a convenient method for defining values that are dependent on just the type, and not on any values within that type. For example, within the new theory of words, the constant dimindex has type :'a itself > num, and returns the cardinality of the universe of the type 'a if the universe is finite, or one otherwise. The syntax support means one can write terms such as dimindex(:bool) and dimindex(:'a > bool) This type is inspired by a similar one in Isabelle/HOL. Bugs fixed: * The muddyC/muddy.c file would not build with gcc4. * The implementation of Q.EXISTS was incorrect (would only work with witnesses of type :bool). Thanks to Eunsuk Kang for the report of this bug. * The natural number and integer decision procedures were not normalising multiplicative expressions as much as they should, causing obvious goals to not get proved. Thanks to Alexey Gotsman for the report of this bug. * The theory and identifier indexes in the help pages were generated with bogus links. Thanks to Hasan Amjad for the report of this bug. * Expressions using caseexpressions with functiontypes and applied to arguments failed to parse correctly. * The implementation of Holmake's rebuild_deps (or r) option was faulty. Thanks to Tom Ridge for the report of this bug. * The implementation of stringLib.string_EQ_CONV failed if one of the string arguments was the empty string. Thanks to Mike Gordon for the report of this bug. * The derivation of "strong" induction principles in the inductive definitions library has been improved to cope with multiple (mutually recursive) inductivelydefined relations. Such relations could always be defined using Hol_reln, but their strong induction principles couldn't be derived. (See below for a change in the type and home of this function.) New theories: * A theory of the rational numbers, thanks to Jens Brandt. This is used in the embedding of ACL2 in HOL. * A new polymorphic theory of fixedwidth words, called words. This is now our recommended way of using types such as word32, word16 etc. This builds on John Harrison's "Finite cartesian products" from A HOL theory of Euclidean space in TPHOLs 2005. There is now no need to use the word functor approach introduced in Kananaskis3 (though this code is still available). Instead, when wordsTheory is loaded, one set of polymorphic constants is defined, and these can be used for all the word types. Words are polymorphic in one argument (thus there is a type ``:'a word``) and types such as word32 and word16 instantiate the type parameter to different concrete type arguments. (The cardinality of the parameter's universe indicates the number of bits in the word.) For more, see the Description. New tools: * None this time! New examples: * A deep embedding of the entire ACL2 logic in HOL has been defined via a theory sexp of Sexpressions. All 78 ACL2 axioms have been verified in HOL. A suite of tools is available to translate HOL datatypes into Sexpressions and HOL functions to functions on Sexpressions. Scripts are provided to print Sexpressions defined inside HOL to defuns and defthms for processing by the ACL2 system, and for slurping ACL2 defuns and defthms into HOL. This work is a collaboration between Mike Gordon and James Reynolds at the University of Cambridge and Warren Hunt and Matt Kaufmann at the University of Texas. The goal is to provide a robust and scalable link between the HOL4 and ACL2 systems suitable for use on substantial industrialscale verification projects. Incompatibilities: * The std_ss simpset has become more powerful, picking up a set of "obvious" rewrites that used to be in arith_ss. Now the latter simpset adds just the decision procedure for Presburger arithmetic. * Functions such as induction_of in the TypeBase structure that used to take a string (the name of a type operator), now take a type. Thus, instead of TypeBase.induction_of "num" use TypeBase.induction_of ``:num`` * The normalisation of arithmetic terms performed by the ARITH_ss simpset fragment (and thus, the simpset bossLib.arith_ss) is more aggressive. This can break proofs. The bossLib library now exports old_arith_ss and old_ARITH_ss entrypoints if users wish to avoid having to adjust their proofs. * The derive_strong_induction function has changed type, and location. It is now an entrypoint in IndDefLib, and has type thm * thm > thm rather than thm list * thm > thm The first argument should now be the "rules" theorem returned by a call to Hol_reln. * In order to avoid certain misleading scenarios, the type of mk_oracle_thm has changed so that it takes a string as its first argument rather than a tag. The implementation of mk_oracle_thm turns the given string into a tag value using the function Tag.read. There is also a new function, Thm.add_tag, that allows arbitrary tags to be added to existing theorems. Thanks to Mark Adams for discussion leading to this change. _________________________________________________________________ HOL 4, Kananaskis4 