1(* Author: Ning Zhang and Christian Urban 2 3Example theory involving Unicode characters (UTF-8 encoding) -- both 4formal and informal ones. 5*) 6 7section \<open>A Chinese theory\<close> 8 9theory Chinese imports Main begin 10 11text\<open>���������������������������������,������������������������������ 12 ������������������������������������������������. 13 14 ������������-������������������������,���������������������,������ 15 ������������������������������������������. 16 17\<close> 18 19datatype shuzi = 20 One ("���") 21 | Two ("���") 22 | Three ("���") 23 | Four ("���") 24 | Five ("���") 25 | Six ("���") 26 | Seven ("���") 27 | Eight ("���") 28 | Nine ("���") 29 | Ten ("���") 30 31primrec translate :: "shuzi \<Rightarrow> nat" ("|_|" [100] 100) where 32 "|���| = 1" 33|"|���| = 2" 34|"|���| = 3" 35|"|���| = 4" 36|"|���| = 5" 37|"|���| = 6" 38|"|���| = 7" 39|"|���| = 8" 40|"|���| = 9" 41|"|���| = 10" 42 43thm translate.simps 44 45lemma "|���| + |���| = |���|" 46 by simp 47 48end 49