--- a/src/HOL/ex/Chinese.thy Wed Sep 21 12:03:41 2005 +0200
+++ b/src/HOL/ex/Chinese.thy Wed Sep 21 13:16:40 2005 +0200
@@ -8,7 +8,7 @@
header {* A Chinese theory *}
-theory Chinese = Main:
+theory Chinese imports Main begin
text{* 数学家能把咖啡变成理论,如今中国的数学家也可
以在伊莎贝拉的帮助下把茶变成理论.