#
80d72112 |
|
16-Aug-2004 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Pretty significant "refactoring" of the early source code. All the stuff that was in common between 0 and experimental-kernel moves into a new prekernel directory. This can be thought of as the kernel utilities directory, full of code that is not quite portableML because it's fairly HOL specific, but that isn't really part of the core implementation of types, terms and theorems. (Also add a new pair_compare function to Lib.)
|