src/HOL/ex/Recdefs.ML
changeset 8683 9d3e8c4a0287
parent 8624 69619f870939
child 9736 332fab43628f
--- a/src/HOL/ex/Recdefs.ML	Fri Apr 07 17:36:56 2000 +0200
+++ b/src/HOL/ex/Recdefs.ML	Sat Apr 08 19:38:19 2000 +0200
@@ -1,6 +1,6 @@
 (*  Title:      HOL/ex/Recdefs.ML
     ID:         $Id$
-    Author:     Konrad Lawrence C Paulson
+    Author:     Konrad Slind and Lawrence C Paulson
     Copyright   1997  University of Cambridge
 
 A few proofs to demonstrate the functions defined in Recdefs.thy