| | No other cites to report in MarkB_generic |
|
| enum1_switch | Def enum1_switch(value;el1;el2;el3) == Switch(value) Case enum1_el1 = > el1 Case enum1_el2 = > el2 Case enum1_el3 = > el3 EndSwitch |
|
| switch_done | Def EndSwitch(x) == !undefined |
|
| enum1_el3 | Def enum1_el3 == 2 |
| | | Thm* enum1_el3  enum1() |
| | | Thm* enum1_el3  |
|
| switch_case | Def Case v = > case cont(x) == if x= v case else cont(x) fi |
|
| enum1_el2 | Def enum1_el2 == 1 |
| | | Thm* enum1_el2 enum1() |
| | | Thm* enum1_el2 |
|
| enum1_el1 | Def enum1_el1 == 0 |
| | | Thm* enum1_el1 enum1() |
| | | Thm* enum1_el1 |
|
| switch | Def Switch(t) b == b(t) |
|
| eq_int | Def i=j == if i=j true ; false fi |
| | | Thm*  i,j:. (i=j)  |
