avoid explicit encoding -- acknowledge UTF-8 as global default and Isabelle/jEdit preference of UTF-8-Isabelle;
authorwenzelm
Mon, 06 Dec 2010 14:45:29 +0100
changeset 40967 5eb59b62e7de
parent 40966 d5a198eb16b5
child 41019 b63cb15e96aa
avoid explicit encoding -- acknowledge UTF-8 as global default and Isabelle/jEdit preference of UTF-8-Isabelle;
src/HOL/ex/Chinese.thy
src/HOL/ex/Hebrew.thy
src/HOL/ex/Serbian.thy
--- a/src/HOL/ex/Chinese.thy	Sun Dec 05 15:23:33 2010 +0100
+++ b/src/HOL/ex/Chinese.thy	Mon Dec 06 14:45:29 2010 +0100
@@ -1,5 +1,4 @@
-(* -*- coding: utf-8 -*- :encoding=utf-8:
-    Author:     Ning Zhang and Christian Urban
+(*  Author:     Ning Zhang and Christian Urban
 
 Example theory involving Unicode characters (UTF-8 encoding) -- both
 formal and informal ones.
--- a/src/HOL/ex/Hebrew.thy	Sun Dec 05 15:23:33 2010 +0100
+++ b/src/HOL/ex/Hebrew.thy	Mon Dec 06 14:45:29 2010 +0100
@@ -1,5 +1,4 @@
-(* -*- coding: utf-8 -*- :encoding=utf-8:  
-    Author:     Makarius
+(*  Author:     Makarius
 
 Example theory involving Unicode characters (UTF-8 encoding) -- both
 formal and informal ones.
--- a/src/HOL/ex/Serbian.thy	Sun Dec 05 15:23:33 2010 +0100
+++ b/src/HOL/ex/Serbian.thy	Mon Dec 06 14:45:29 2010 +0100
@@ -1,5 +1,4 @@
-(* -*- coding: utf-8 -*- :encoding=utf-8:  
-    Author:     Filip Maric
+(*  Author:     Filip Maric
 
 Example theory involving Unicode characters (UTF-8 encoding) -- 
 Conversion between Serbian cyrillic and latin letters (српска ћирилица и латиница)