| 1997-11-03 | wenzelm | adapted to new datatypes thy info; | file | diff | annotate |
| 1997-06-05 | paulson | Numerous simplifications and removal of HOL-isms | file | diff | annotate |
| 1997-06-03 | paulson | More de-HOLification: using Free, Const, etc. instead of mk_var, mk_const | file | diff | annotate |
| 1997-06-02 | paulson | Type inference makes a Const here, perhaps elsewhere?thry.sml | file | diff | annotate |
| 1997-05-27 | paulson | Removal of module Mask and datatype binding with its constructor |-> | file | diff | annotate |
| 1997-05-26 | paulson | More de-HOL-ification | file | diff | annotate |
| 1997-05-22 | paulson | New headers and other minor changes | file | diff | annotate |
| 1997-05-20 | paulson | Removal of redundant code (unused or already present in Isabelle. | file | diff | annotate |
| 1997-05-15 | paulson | TFL now integrated with HOL (more work needed) | file | diff | annotate |
| 1996-10-18 | paulson | Konrad Slind's TFL | file | diff | annotate |