src/HOL/ex/Chinese.thy
changeset 17553 d7b304d05956
parent 17505 928bd7053d6a
child 24312 bb5ec06f7c7a
equal deleted inserted replaced
17552:744924bec974 17553:d7b304d05956
     6 formal and informal ones.
     6 formal and informal ones.
     7 *)
     7 *)
     8 
     8 
     9 header {* A Chinese theory *}
     9 header {* A Chinese theory *}
    10 
    10 
    11 theory Chinese = Main:
    11 theory Chinese imports Main begin
    12 
    12 
    13 text{* 数学家能把咖啡变成理论,如今中国的数学家也可
    13 text{* 数学家能把咖啡变成理论,如今中国的数学家也可
    14        以在伊莎贝拉的帮助下把茶变成理论.  
    14        以在伊莎贝拉的帮助下把茶变成理论.  
    15 
    15 
    16        伊莎贝拉-世界数学家的新宠,现今能识别中文,成为
    16        伊莎贝拉-世界数学家的新宠,现今能识别中文,成为