changeset 62058 | 1cfd5d604937 |
parent 61814 | 1ca1142e1711 |
child 63239 | d562c9948dee |
--- a/src/HOL/Library/old_recdef.ML Tue Jan 05 13:41:29 2016 +0100 +++ b/src/HOL/Library/old_recdef.ML Tue Jan 05 13:48:51 2016 +0100 @@ -1,4 +1,4 @@ -(* Title: HOL/Tools/old_recdef.ML +(* Title: HOL/Library/old_recdef.ML Author: Konrad Slind, Cambridge University Computer Laboratory Author: Lucas Dixon, University of Edinburgh