changeset 9421 | d8dfa816a368 |
parent 9399 | effc8d44c89c |
child 9736 | 332fab43628f |
--- a/src/HOL/Finite.ML Mon Jul 24 23:48:29 2000 +0200 +++ b/src/HOL/Finite.ML Mon Jul 24 23:51:11 2000 +0200 @@ -1,9 +1,9 @@ -(* Title: HOL/Finite.thy +(* Title: HOL/Finite.ML ID: $Id$ Author: Lawrence C Paulson & Tobias Nipkow Copyright 1995 University of Cambridge & TU Muenchen -Finite sets and their cardinality +Finite sets and their cardinality. *) section "finite";