equal
deleted
inserted
replaced
8 header {* Cardinal Arithmetic *} |
8 header {* Cardinal Arithmetic *} |
9 |
9 |
10 theory Cardinal_Arithmetic |
10 theory Cardinal_Arithmetic |
11 imports BNF_Cardinal_Arithmetic Cardinal_Order_Relation |
11 imports BNF_Cardinal_Arithmetic Cardinal_Order_Relation |
12 begin |
12 begin |
13 |
|
14 notation |
|
15 csum (infixr "+c" 65) and |
|
16 cprod (infixr "*c" 80) and |
|
17 cexp (infixr "^c" 90) |
|
18 |
|
19 |
13 |
20 subsection {* Binary sum *} |
14 subsection {* Binary sum *} |
21 |
15 |
22 lemma csum_Cnotzero2: |
16 lemma csum_Cnotzero2: |
23 "Cnotzero r2 \<Longrightarrow> Cnotzero (r1 +c r2)" |
17 "Cnotzero r2 \<Longrightarrow> Cnotzero (r1 +c r2)" |