changeset 3302 | 404fe31fd8d2 |
parent 3273 | 114704740c86 |
child 3458 | 5ff4bfab859c |
--- a/TFL/thms.sml Thu May 22 15:11:56 1997 +0200 +++ b/TFL/thms.sml Thu May 22 15:13:16 1997 +0200 @@ -1,3 +1,9 @@ +(* Title: TFL/thms + ID: $Id$ + Author: Konrad Slind, Cambridge University Computer Laboratory + Copyright 1997 University of Cambridge +*) + structure Thms : Thms_sig = struct val WFREC_COROLLARY = get_thm WF_Rel.thy "tfl_wfrec"