changeset 1476 | 608483c2122a |
parent 1376 | 92f83b9d17e1 |
child 1789 | aade046ec6d5 |
--- a/src/HOL/ex/Perm.thy Mon Feb 05 21:27:16 1996 +0100 +++ b/src/HOL/ex/Perm.thy Mon Feb 05 21:29:06 1996 +0100 @@ -1,6 +1,6 @@ -(* Title: HOL/ex/Perm.thy +(* Title: HOL/ex/Perm.thy ID: $Id$ - Author: Lawrence C Paulson, Cambridge University Computer Laboratory + Author: Lawrence C Paulson, Cambridge University Computer Laboratory Copyright 1995 University of Cambridge Permutations: example of an inductive definition