equal
deleted
inserted
replaced
9 |
9 |
10 theory Constructions_on_Wellorders |
10 theory Constructions_on_Wellorders |
11 imports BNF_Constructions_on_Wellorders Wellorder_Embedding Order_Union |
11 imports BNF_Constructions_on_Wellorders Wellorder_Embedding Order_Union |
12 begin |
12 begin |
13 |
13 |
14 notation ordLeq2 (infix "<=o" 50) and |
14 notation |
|
15 ordLeq2 (infix "<=o" 50) and |
15 ordLeq3 (infix "\<le>o" 50) and |
16 ordLeq3 (infix "\<le>o" 50) and |
16 ordLess2 (infix "<o" 50) and |
17 ordLess2 (infix "<o" 50) and |
17 ordIso2 (infix "=o" 50) |
18 ordIso2 (infix "=o" 50) |
18 |
19 |
19 declare |
20 declare |