src/ZF/Finite.thy
changeset 1155 928a16e02f9f
parent 806 6330ca0a3ac5
child 1401 0c439768f45c
     1.1 --- a/src/ZF/Finite.thy	Thu Jun 22 12:58:39 1995 +0200
     1.2 +++ b/src/ZF/Finite.thy	Thu Jun 22 17:13:05 1995 +0200
     1.3 @@ -23,7 +23,7 @@
     1.4    domains   "FiniteFun(A,B)" <= "Fin(A*B)"
     1.5    intrs
     1.6      emptyI  "0 : A -||> B"
     1.7 -    consI   "[| a: A;  b: B;  h: A -||> B;  a ~: domain(h)   \
     1.8 -\	     |] ==> cons(<a,b>,h) : A -||> B"
     1.9 +    consI   "[| a: A;  b: B;  h: A -||> B;  a ~: domain(h)   
    1.10 +	     |] ==> cons(<a,b>,h) : A -||> B"
    1.11    type_intrs "Fin.intrs"
    1.12  end