src/ZF/ex/Acc.thy
changeset 6117 f9aad8ccd590
parent 1478 2b8c2a7547ab
child 11316 b4e71bd751e4
     1.1 --- a/src/ZF/ex/Acc.thy	Wed Jan 13 12:44:33 1999 +0100
     1.2 +++ b/src/ZF/ex/Acc.thy	Wed Jan 13 15:14:47 1999 +0100
     1.3 @@ -18,6 +18,6 @@
     1.4    domains "acc(r)" <= "field(r)"
     1.5    intrs
     1.6      vimage  "[| r-``{a}: Pow(acc(r)); a: field(r) |] ==> a: acc(r)"
     1.7 -  monos     "[Pow_mono]"
     1.8 +  monos      Pow_mono
     1.9  
    1.10  end