| changeset 11539 | 0f17da240450 |
| parent 11537 | e007d35359c3 |
| child 12453 | 806502073957 |
--- a/src/HOL/Tools/inductive_codegen.ML Fri Aug 31 18:43:27 2001 +0200 +++ b/src/HOL/Tools/inductive_codegen.ML Fri Aug 31 18:46:48 2001 +0200 @@ -1,9 +1,9 @@ (* Title: Pure/HOL/inductive_codegen.ML ID: $Id$ - Author: Stefan Berghofer - Copyright 2000 TU Muenchen + Author: Stefan Berghofer, TU Muenchen + License: GPL (GNU GENERAL PUBLIC LICENSE) -Code generator for inductive predicates +Code generator for inductive predicates. *) signature INDUCTIVE_CODEGEN =