equal
deleted
inserted
replaced
2 |
2 |
3 Example theory involving Unicode characters (UTF-8 encoding) -- both |
3 Example theory involving Unicode characters (UTF-8 encoding) -- both |
4 formal and informal ones. |
4 formal and informal ones. |
5 *) |
5 *) |
6 |
6 |
7 header {* A Chinese theory *} |
7 section {* A Chinese theory *} |
8 |
8 |
9 theory Chinese imports Main begin |
9 theory Chinese imports Main begin |
10 |
10 |
11 text{* 数学家能把咖啡变成理论,如今中国的数学家也可 |
11 text{* 数学家能把咖啡变成理论,如今中国的数学家也可 |
12 以在伊莎贝拉的帮助下把茶变成理论. |
12 以在伊莎贝拉的帮助下把茶变成理论. |