src/HOL/String.thy

--- a/src/HOL/String.thy	Fri Mar 18 22:19:46 2016 +0100
+++ b/src/HOL/String.thy	Sat Mar 19 16:53:09 2016 +0100
@@ -206,9 +206,7 @@
 
 syntax
   "_Char" :: "str_position \<Rightarrow> char"    ("CHR _")
-
-syntax
-  "_Char_ord" :: "num_const \<Rightarrow> char"     ("CHAR _")
+  "_Char_ord" :: "num_const \<Rightarrow> char"   ("CHR _")
 
 type_synonym string = "char list"
 
@@ -221,16 +219,16 @@
 begin
 
 definition
-  "Enum.enum = [0, CHAR 0x01, CHAR 0x02, CHAR 0x03,
-    CHAR 0x04, CHAR 0x05, CHAR 0x06, CHAR 0x07,
-    CHAR 0x08, CHAR 0x09, CHR ''\<newline>'', CHAR 0x0B,
-    CHAR 0x0C, CHAR 0x0D, CHAR 0x0E, CHAR 0x0F,
-    CHAR 0x10, CHAR 0x11, CHAR 0x12, CHAR 0x13,
-    CHAR 0x14, CHAR 0x15, CHAR 0x16, CHAR 0x17,
-    CHAR 0x18, CHAR 0x19, CHAR 0x1A, CHAR 0x1B,
-    CHAR 0x1C, CHAR 0x1D, CHAR 0x1E, CHAR 0x1F,
-    CHR '' '', CHR ''!'', CHAR 0x22, CHR ''#'',
-    CHR ''$'', CHR ''%'', CHR ''&'', CHAR 0x27,
+  "Enum.enum = [0, CHR 0x01, CHR 0x02, CHR 0x03,
+    CHR 0x04, CHR 0x05, CHR 0x06, CHR 0x07,
+    CHR 0x08, CHR 0x09, CHR ''\<newline>'', CHR 0x0B,
+    CHR 0x0C, CHR 0x0D, CHR 0x0E, CHR 0x0F,
+    CHR 0x10, CHR 0x11, CHR 0x12, CHR 0x13,
+    CHR 0x14, CHR 0x15, CHR 0x16, CHR 0x17,
+    CHR 0x18, CHR 0x19, CHR 0x1A, CHR 0x1B,
+    CHR 0x1C, CHR 0x1D, CHR 0x1E, CHR 0x1F,
+    CHR '' '', CHR ''!'', CHR 0x22, CHR ''#'',
+    CHR ''$'', CHR ''%'', CHR ''&'', CHR 0x27,
     CHR ''('', CHR '')'', CHR ''*'', CHR ''+'',
     CHR '','', CHR ''-'', CHR ''.'', CHR ''/'',
     CHR ''0'', CHR ''1'', CHR ''2'', CHR ''3'',
@@ -244,47 +242,47 @@
     CHR ''P'', CHR ''Q'', CHR ''R'', CHR ''S'',
     CHR ''T'', CHR ''U'', CHR ''V'', CHR ''W'',
     CHR ''X'', CHR ''Y'', CHR ''Z'', CHR ''['',
-    CHAR 0x5C, CHR '']'', CHR ''^'', CHR ''_'',
-    CHAR 0x60, CHR ''a'', CHR ''b'', CHR ''c'',
+    CHR 0x5C, CHR '']'', CHR ''^'', CHR ''_'',
+    CHR 0x60, CHR ''a'', CHR ''b'', CHR ''c'',
     CHR ''d'', CHR ''e'', CHR ''f'', CHR ''g'',
     CHR ''h'', CHR ''i'', CHR ''j'', CHR ''k'',
     CHR ''l'', CHR ''m'', CHR ''n'', CHR ''o'',
     CHR ''p'', CHR ''q'', CHR ''r'', CHR ''s'',
     CHR ''t'', CHR ''u'', CHR ''v'', CHR ''w'',
     CHR ''x'', CHR ''y'', CHR ''z'', CHR ''{'',
-    CHR ''|'', CHR ''}'', CHR ''~'', CHAR 0x7F,
-    CHAR 0x80, CHAR 0x81, CHAR 0x82, CHAR 0x83,
-    CHAR 0x84, CHAR 0x85, CHAR 0x86, CHAR 0x87,
-    CHAR 0x88, CHAR 0x89, CHAR 0x8A, CHAR 0x8B,
-    CHAR 0x8C, CHAR 0x8D, CHAR 0x8E, CHAR 0x8F,
-    CHAR 0x90, CHAR 0x91, CHAR 0x92, CHAR 0x93,
-    CHAR 0x94, CHAR 0x95, CHAR 0x96, CHAR 0x97,
-    CHAR 0x98, CHAR 0x99, CHAR 0x9A, CHAR 0x9B,
-    CHAR 0x9C, CHAR 0x9D, CHAR 0x9E, CHAR 0x9F,
-    CHAR 0xA0, CHAR 0xA1, CHAR 0xA2, CHAR 0xA3,
-    CHAR 0xA4, CHAR 0xA5, CHAR 0xA6, CHAR 0xA7,
-    CHAR 0xA8, CHAR 0xA9, CHAR 0xAA, CHAR 0xAB,
-    CHAR 0xAC, CHAR 0xAD, CHAR 0xAE, CHAR 0xAF,
-    CHAR 0xB0, CHAR 0xB1, CHAR 0xB2, CHAR 0xB3,
-    CHAR 0xB4, CHAR 0xB5, CHAR 0xB6, CHAR 0xB7,
-    CHAR 0xB8, CHAR 0xB9, CHAR 0xBA, CHAR 0xBB,
-    CHAR 0xBC, CHAR 0xBD, CHAR 0xBE, CHAR 0xBF,
-    CHAR 0xC0, CHAR 0xC1, CHAR 0xC2, CHAR 0xC3,
-    CHAR 0xC4, CHAR 0xC5, CHAR 0xC6, CHAR 0xC7,
-    CHAR 0xC8, CHAR 0xC9, CHAR 0xCA, CHAR 0xCB,
-    CHAR 0xCC, CHAR 0xCD, CHAR 0xCE, CHAR 0xCF,
-    CHAR 0xD0, CHAR 0xD1, CHAR 0xD2, CHAR 0xD3,
-    CHAR 0xD4, CHAR 0xD5, CHAR 0xD6, CHAR 0xD7,
-    CHAR 0xD8, CHAR 0xD9, CHAR 0xDA, CHAR 0xDB,
-    CHAR 0xDC, CHAR 0xDD, CHAR 0xDE, CHAR 0xDF,
-    CHAR 0xE0, CHAR 0xE1, CHAR 0xE2, CHAR 0xE3,
-    CHAR 0xE4, CHAR 0xE5, CHAR 0xE6, CHAR 0xE7,
-    CHAR 0xE8, CHAR 0xE9, CHAR 0xEA, CHAR 0xEB,
-    CHAR 0xEC, CHAR 0xED, CHAR 0xEE, CHAR 0xEF,
-    CHAR 0xF0, CHAR 0xF1, CHAR 0xF2, CHAR 0xF3,
-    CHAR 0xF4, CHAR 0xF5, CHAR 0xF6, CHAR 0xF7,
-    CHAR 0xF8, CHAR 0xF9, CHAR 0xFA, CHAR 0xFB,
-    CHAR 0xFC, CHAR 0xFD, CHAR 0xFE, CHAR 0xFF]"
+    CHR ''|'', CHR ''}'', CHR ''~'', CHR 0x7F,
+    CHR 0x80, CHR 0x81, CHR 0x82, CHR 0x83,
+    CHR 0x84, CHR 0x85, CHR 0x86, CHR 0x87,
+    CHR 0x88, CHR 0x89, CHR 0x8A, CHR 0x8B,
+    CHR 0x8C, CHR 0x8D, CHR 0x8E, CHR 0x8F,
+    CHR 0x90, CHR 0x91, CHR 0x92, CHR 0x93,
+    CHR 0x94, CHR 0x95, CHR 0x96, CHR 0x97,
+    CHR 0x98, CHR 0x99, CHR 0x9A, CHR 0x9B,
+    CHR 0x9C, CHR 0x9D, CHR 0x9E, CHR 0x9F,
+    CHR 0xA0, CHR 0xA1, CHR 0xA2, CHR 0xA3,
+    CHR 0xA4, CHR 0xA5, CHR 0xA6, CHR 0xA7,
+    CHR 0xA8, CHR 0xA9, CHR 0xAA, CHR 0xAB,
+    CHR 0xAC, CHR 0xAD, CHR 0xAE, CHR 0xAF,
+    CHR 0xB0, CHR 0xB1, CHR 0xB2, CHR 0xB3,
+    CHR 0xB4, CHR 0xB5, CHR 0xB6, CHR 0xB7,
+    CHR 0xB8, CHR 0xB9, CHR 0xBA, CHR 0xBB,
+    CHR 0xBC, CHR 0xBD, CHR 0xBE, CHR 0xBF,
+    CHR 0xC0, CHR 0xC1, CHR 0xC2, CHR 0xC3,
+    CHR 0xC4, CHR 0xC5, CHR 0xC6, CHR 0xC7,
+    CHR 0xC8, CHR 0xC9, CHR 0xCA, CHR 0xCB,
+    CHR 0xCC, CHR 0xCD, CHR 0xCE, CHR 0xCF,
+    CHR 0xD0, CHR 0xD1, CHR 0xD2, CHR 0xD3,
+    CHR 0xD4, CHR 0xD5, CHR 0xD6, CHR 0xD7,
+    CHR 0xD8, CHR 0xD9, CHR 0xDA, CHR 0xDB,
+    CHR 0xDC, CHR 0xDD, CHR 0xDE, CHR 0xDF,
+    CHR 0xE0, CHR 0xE1, CHR 0xE2, CHR 0xE3,
+    CHR 0xE4, CHR 0xE5, CHR 0xE6, CHR 0xE7,
+    CHR 0xE8, CHR 0xE9, CHR 0xEA, CHR 0xEB,
+    CHR 0xEC, CHR 0xED, CHR 0xEE, CHR 0xEF,
+    CHR 0xF0, CHR 0xF1, CHR 0xF2, CHR 0xF3,
+    CHR 0xF4, CHR 0xF5, CHR 0xF6, CHR 0xF7,
+    CHR 0xF8, CHR 0xF9, CHR 0xFA, CHR 0xFB,
+    CHR 0xFC, CHR 0xFD, CHR 0xFE, CHR 0xFF]"
 
 definition
   "Enum.enum_all P \<longleftrightarrow> list_all P (Enum.enum :: char list)"