src/ZF/CardinalArith.thy
changeset 753 ec86863e87c8
parent 516 1957113f0d7d
child 827 aa332949ce1a
     1.1 --- a/src/ZF/CardinalArith.thy	Mon Nov 28 19:48:30 1994 +0100
     1.2 +++ b/src/ZF/CardinalArith.thy	Tue Nov 29 00:31:31 1994 +0100
     1.3 @@ -16,7 +16,7 @@
     1.4    jump_cardinal :: "i=>i"
     1.5    csucc       :: "i=>i"
     1.6  
     1.7 -rules
     1.8 +defs
     1.9  
    1.10    InfCard_def  "InfCard(i) == Card(i) & nat le i"
    1.11