changeset 1475 | 7f5a4cd08209 |
parent 1370 | 7361ac9b024d |
child 1531 | e5eb247ad13c |
--- a/src/HOL/Finite.thy Mon Feb 05 14:44:09 1996 +0100 +++ b/src/HOL/Finite.thy Mon Feb 05 21:27:16 1996 +0100 @@ -1,6 +1,6 @@ -(* Title: HOL/Finite.thy +(* Title: HOL/Finite.thy ID: $Id$ - Author: Lawrence C Paulson, Cambridge University Computer Laboratory + Author: Lawrence C Paulson, Cambridge University Computer Laboratory Copyright 1994 University of Cambridge Finite powerset operator