# HG changeset patch
# User wenzelm
# Date 1127301400 -7200
# Node ID d7b304d05956aff758493b79bf9aea66eb47ee7d
# Parent  744924bec9745aecce3ad6f5815ab8db3cc15f62
isatool fixheaders;

diff -r 744924bec974 -r d7b304d05956 src/HOL/ex/Chinese.thy
--- 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{* 数学家能把咖啡变成理论,如今中国的数学家也可
        以在伊莎贝拉的帮助下把茶变成理论.