# HG changeset patch
# User wenzelm
# Date 1127217394 -7200
# Node ID 928bd7053d6a85edd3da4c8c38239c715a5c2376
# Parent  cc10c4b64b8e12e34916d727ba67dcea15235bc2
Chinese Unicode example;

diff -r cc10c4b64b8e -r 928bd7053d6a src/HOL/ex/Chinese.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/ex/Chinese.thy	Tue Sep 20 13:56:34 2005 +0200
@@ -0,0 +1,53 @@
+(* -*- coding: utf-8 -*-
+    ID:         $Id$
+    Author:     Ning Zhang and Christian Urban
+
+Example theory involving Unicode characters (UTF-8 encoding) -- both
+formal and informal ones.
+*)
+
+header {* A Chinese theory *}
+
+theory Chinese = Main:
+
+text{* 数学家能把咖啡变成理论,如今中国的数学家也可
+       以在伊莎贝拉的帮助下把茶变成理论.  
+
+       伊莎贝拉-世界数学家的新宠,现今能识别中文,成为
+       中国数学家理论推导的得力助手.
+
+    *}
+
+datatype shuzi =
+    One   ("一")
+  | Two   ("二")
+  | Three ("三") 
+  | Four  ("四")
+  | Five  ("五")
+  | Six   ("六")
+  | Seven ("七")
+  | Eight ("八")
+  | Nine  ("九")
+  | Ten   ("十")
+
+consts
+  translate :: "shuzi \<Rightarrow> nat" ("|_|" [100] 100)
+
+primrec
+ "|一| = 1"
+ "|二| = 2"
+ "|三| = 3"
+ "|四| = 4"
+ "|五| = 5"
+ "|六| = 6"
+ "|七| = 7"
+ "|八| = 8"
+ "|九| = 9"
+ "|十| = 10"
+
+thm translate.simps
+
+lemma "|四| + |六| = |十|"
+  by simp 
+
+end
diff -r cc10c4b64b8e -r 928bd7053d6a src/HOL/ex/ROOT.ML
--- a/src/HOL/ex/ROOT.ML	Tue Sep 20 13:56:01 2005 +0200
+++ b/src/HOL/ex/ROOT.ML	Tue Sep 20 13:56:34 2005 +0200
@@ -52,3 +52,4 @@
 time_use_thy "Adder";
 
 HTML.with_charset "utf-8" (no_document time_use_thy) "Hebrew";
+HTML.with_charset "utf-8" (no_document time_use_thy) "Chinese";