src/ZF/ZF.thy
changeset 55380 4de48353034e
parent 48733 18e76e2db6d4
child 58871 c399ae4b836f
     1.1 --- a/src/ZF/ZF.thy	Mon Feb 10 14:33:47 2014 +0100
     1.2 +++ b/src/ZF/ZF.thy	Mon Feb 10 17:20:11 2014 +0100
     1.3 @@ -12,7 +12,7 @@
     1.4  declare [[eta_contract = false]]
     1.5  
     1.6  typedecl i
     1.7 -arities  i :: "term"
     1.8 +instance i :: "term" ..
     1.9  
    1.10  axiomatization
    1.11    zero :: "i"  ("0")   --{*the empty set*}  and