src/ZF/CardinalArith.thy
changeset 9654 9754ba005b64
parent 9548 15bee2731e43
child 9683 f87c8c449018
     1.1 --- a/src/ZF/CardinalArith.thy	Fri Aug 18 18:11:10 2000 +0200
     1.2 +++ b/src/ZF/CardinalArith.thy	Fri Aug 18 18:46:02 2000 +0200
     1.3 @@ -39,4 +39,7 @@
     1.4    (*needed because jump_cardinal(K) might not be the successor of K*)
     1.5    csucc_def "csucc(K) == LEAST L. Card(L) & K<L"
     1.6  
     1.7 +syntax (symbols)
     1.8 +  "op |*|"     :: [i,i] => i          (infixr "|\\<times>|" 70)
     1.9 +
    1.10  end