changeset 46506 | c7faa011bfa7 |
parent 44890 | 22f665a2e91c |
child 46512 | 4f9f61f9b535 |
46505:cefceb54c656 | 46506:c7faa011bfa7 |
---|---|
5 |
5 |
6 header {* Abstract commutation and confluence notions *} |
6 header {* Abstract commutation and confluence notions *} |
7 |
7 |
8 theory Commutation imports Main begin |
8 theory Commutation imports Main begin |
9 |
9 |
10 declare [[syntax_ambiguity_level = 100]] |
10 declare [[syntax_ambiguity = ignore]] |
11 |
11 |
12 |
12 |
13 subsection {* Basic definitions *} |
13 subsection {* Basic definitions *} |
14 |
14 |
15 definition |
15 definition |