Chinese Unicode example;
authorwenzelm
Tue Sep 20 13:56:34 2005 +0200 (2005-09-20)
changeset 17505928bd7053d6a
parent 17504 cc10c4b64b8e
child 17506 f20e5c8433a4
Chinese Unicode example;
src/HOL/ex/Chinese.thy
src/HOL/ex/ROOT.ML
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/ex/Chinese.thy	Tue Sep 20 13:56:34 2005 +0200
     1.3 @@ -0,0 +1,53 @@
     1.4 +(* -*- coding: utf-8 -*-
     1.5 +    ID:         $Id$
     1.6 +    Author:     Ning Zhang and Christian Urban
     1.7 +
     1.8 +Example theory involving Unicode characters (UTF-8 encoding) -- both
     1.9 +formal and informal ones.
    1.10 +*)
    1.11 +
    1.12 +header {* A Chinese theory *}
    1.13 +
    1.14 +theory Chinese = Main:
    1.15 +
    1.16 +text{* 数学家能把咖啡变成理论,如今中国的数学家也可
    1.17 +       以在伊莎贝拉的帮助下把茶变成理论.  
    1.18 +
    1.19 +       伊莎贝拉-世界数学家的新宠,现今能识别中文,成为
    1.20 +       中国数学家理论推导的得力助手.
    1.21 +
    1.22 +    *}
    1.23 +
    1.24 +datatype shuzi =
    1.25 +    One   ("一")
    1.26 +  | Two   ("二")
    1.27 +  | Three ("三") 
    1.28 +  | Four  ("四")
    1.29 +  | Five  ("五")
    1.30 +  | Six   ("六")
    1.31 +  | Seven ("七")
    1.32 +  | Eight ("八")
    1.33 +  | Nine  ("九")
    1.34 +  | Ten   ("十")
    1.35 +
    1.36 +consts
    1.37 +  translate :: "shuzi \<Rightarrow> nat" ("|_|" [100] 100)
    1.38 +
    1.39 +primrec
    1.40 + "|一| = 1"
    1.41 + "|二| = 2"
    1.42 + "|三| = 3"
    1.43 + "|四| = 4"
    1.44 + "|五| = 5"
    1.45 + "|六| = 6"
    1.46 + "|七| = 7"
    1.47 + "|八| = 8"
    1.48 + "|九| = 9"
    1.49 + "|十| = 10"
    1.50 +
    1.51 +thm translate.simps
    1.52 +
    1.53 +lemma "|四| + |六| = |十|"
    1.54 +  by simp 
    1.55 +
    1.56 +end
     2.1 --- a/src/HOL/ex/ROOT.ML	Tue Sep 20 13:56:01 2005 +0200
     2.2 +++ b/src/HOL/ex/ROOT.ML	Tue Sep 20 13:56:34 2005 +0200
     2.3 @@ -52,3 +52,4 @@
     2.4  time_use_thy "Adder";
     2.5  
     2.6  HTML.with_charset "utf-8" (no_document time_use_thy) "Hebrew";
     2.7 +HTML.with_charset "utf-8" (no_document time_use_thy) "Chinese";