--- a/src/ZF/AC.thy Mon Feb 05 21:33:14 1996 +0100
+++ b/src/ZF/AC.thy Tue Feb 06 12:27:17 1996 +0100
@@ -1,6 +1,6 @@
-(* Title: ZF/AC.thy
+(* Title: ZF/AC.thy
ID: $Id$
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1994 University of Cambridge
The Axiom of Choice
@@ -10,5 +10,5 @@
AC = ZF + "func" +
rules
- AC "[| a: A; !!x. x:A ==> (EX y. y:B(x)) |] ==> EX z. z : Pi(A,B)"
+ AC "[| a: A; !!x. x:A ==> (EX y. y:B(x)) |] ==> EX z. z : Pi(A,B)"
end