src/ZF/Perm.thy
 changeset 1478 2b8c2a7547ab parent 1401 0c439768f45c child 1806 12708740f58d
```--- a/src/ZF/Perm.thy	Mon Feb 05 21:33:14 1996 +0100
+++ b/src/ZF/Perm.thy	Tue Feb 06 12:27:17 1996 +0100
@@ -1,6 +1,6 @@
-(*  Title: 	ZF/perm
+(*  Title:      ZF/perm
ID:         \$Id\$
-    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
+    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory

The theory underlying permutation groups
@@ -11,26 +11,26 @@

Perm = ZF + "mono" +
consts
-    O    	::      [i,i]=>i      (infixr 60)
-    id  	::      i=>i
+    O           ::      [i,i]=>i      (infixr 60)
+    id          ::      i=>i
inj,surj,bij::      [i,i]=>i

defs

(*composition of relations and functions; NOT Suppes's relative product*)
-    comp_def	"r O s == {xz : domain(s)*range(r) .
-                  		EX x y z. xz=<x,z> & <x,y>:s & <y,z>:r}"
+    comp_def    "r O s == {xz : domain(s)*range(r) .
+                                EX x y z. xz=<x,z> & <x,y>:s & <y,z>:r}"

(*the identity function for A*)
-    id_def	"id(A) == (lam x:A. x)"
+    id_def      "id(A) == (lam x:A. x)"

(*one-to-one functions from A to B*)
inj_def      "inj(A,B) == { f: A->B. ALL w:A. ALL x:A. f`w=f`x --> w=x}"

(*onto functions from A to B*)
-    surj_def	"surj(A,B) == { f: A->B . ALL y:B. EX x:A. f`x=y}"
+    surj_def    "surj(A,B) == { f: A->B . ALL y:B. EX x:A. f`x=y}"

(*one-to-one and onto functions*)
-    bij_def	"bij(A,B) == inj(A,B) Int surj(A,B)"
+    bij_def     "bij(A,B) == inj(A,B) Int surj(A,B)"

end```