src/ZF/Finite.thy
changeset 1401 0c439768f45c
parent 1155 928a16e02f9f
child 1478 2b8c2a7547ab
     1.1 --- a/src/ZF/Finite.thy	Fri Dec 08 19:48:15 1995 +0100
     1.2 +++ b/src/ZF/Finite.thy	Sat Dec 09 13:36:11 1995 +0100
     1.3 @@ -8,8 +8,8 @@
     1.4  
     1.5  Finite = Arith + Inductive +
     1.6  consts
     1.7 -  Fin 	    :: "i=>i"
     1.8 -  FiniteFun :: "[i,i]=>i"		("(_ -||>/ _)" [61, 60] 60)
     1.9 +  Fin 	    :: i=>i
    1.10 +  FiniteFun :: [i,i]=>i		("(_ -||>/ _)" [61, 60] 60)
    1.11  
    1.12  inductive
    1.13    domains   "Fin(A)" <= "Pow(A)"