changeset 1465 | 5d7a7e439cec |
parent 1455 | 52a0271621f3 |
child 1657 | a7a6c3fb3cdd |
--- a/src/HOL/thy_data.ML Tue Jan 30 15:19:20 1996 +0100 +++ b/src/HOL/thy_data.ML Tue Jan 30 15:24:36 1996 +0100 @@ -1,6 +1,6 @@ -(* Title: HOL/thy_data.ML +(* Title: HOL/thy_data.ML ID: $Id$ - Author: Carsten Clasohm + Author: Carsten Clasohm Copyright 1995 TU Muenchen Definitions that have to be reread after init_thy_reader has been invoked