improved handling of single-quoted names;

--- a/src/HOL/TPTP/TPTP_Parser/tptp.lex	Mon Apr 23 12:23:23 2012 +0100
+++ b/src/HOL/TPTP/TPTP_Parser/tptp.lex	Mon Apr 23 12:23:23 2012 +0100
@@ -54,9 +54,9 @@
 
 percentage_sign           = "%";
 double_quote              = ["];
-do_char                   = ([^"]|[\\]["\\]);
+do_char                   = ([^"\\]|[\\]["\\]);
 single_quote              = ['];
-sq_char                   = ([\040-\041\043-\126]|[\\]['\\]);
+sq_char                   = ([^'\\]|[\\]['\\]);
 sign                      = [+-];
 dot                       = [.];
 exponent                  = [Ee];
@@ -90,7 +90,7 @@
 distinct_object           = {double_quote}{do_char}+{double_quote};
 
 ws                        = ([\ ]|[\t]);
-single_quoted             = {single_quote}({alpha_numeric}|{sq_char}|{ws})+{single_quote};
+single_quoted             = {single_quote}{sq_char}+{single_quote};
 
 system_comment_one        = [%][\ ]*{ddollar}[_]*;
 system_comment_multi      = [/][\*][\ ]*(ddollar)([^\*]*[\*][\*]*[^/\*])*[^\*]*[\*][\*]*[/];

--- a/src/HOL/TPTP/TPTP_Parser/tptp.yacc	Mon Apr 23 12:23:23 2012 +0100
+++ b/src/HOL/TPTP/TPTP_Parser/tptp.yacc	Mon Apr 23 12:23:23 2012 +0100
@@ -836,7 +836,7 @@
      | integer     (( integer ))
 
 atomic_word : LOWER_WORD    (( LOWER_WORD ))
-            | SINGLE_QUOTED (( SINGLE_QUOTED ))
+            | SINGLE_QUOTED (( dequote SINGLE_QUOTED ))
             | THF           (( "thf" ))
             | TFF           (( "tff" ))
             | FOF           (( "fof" ))

--- a/src/HOL/TPTP/TPTP_Parser/tptp_lexyacc.ML	Mon Apr 23 12:23:23 2012 +0100
+++ b/src/HOL/TPTP/TPTP_Parser/tptp_lexyacc.ML	Mon Apr 23 12:23:23 2012 +0100
@@ -174,9 +174,9 @@
 \\000"
 ),
  (1, 
-"\000\000\000\000\000\000\000\000\000\144\146\000\000\145\000\000\
-\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
-\\144\140\134\000\102\090\089\083\082\081\080\078\077\072\070\057\
+"\000\000\000\000\000\000\000\000\000\142\144\000\000\143\000\000\
+\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
+\\142\138\133\000\101\089\088\083\082\081\080\078\077\072\070\057\
 \\048\048\048\048\048\048\048\048\048\048\045\000\039\037\036\033\
 \\030\029\029\029\029\029\029\029\029\029\029\029\029\029\029\029\
 \\029\029\029\029\029\029\029\029\029\029\029\028\000\027\026\000\
@@ -702,427 +702,427 @@
 \\000"
 ),
  (83, 
-"\000\000\000\000\000\000\000\000\000\084\000\000\000\000\000\000\
-\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
-\\084\000\000\000\000\000\000\000\084\084\000\084\084\084\084\084\
+"\084\084\084\084\084\084\084\084\084\084\084\084\084\084\084\084\
+\\084\084\084\084\084\084\084\084\084\084\084\084\084\084\084\084\
+\\084\084\084\084\084\084\084\000\084\084\084\084\084\084\084\084\
 \\084\084\084\084\084\084\084\084\084\084\084\084\084\084\084\084\
 \\084\084\084\084\084\084\084\084\084\084\084\084\084\084\084\084\
-\\084\084\084\084\084\084\084\084\084\084\084\084\088\084\084\084\
+\\084\084\084\084\084\084\084\084\084\084\084\084\087\084\084\084\
 \\084\084\084\084\084\084\084\084\084\084\084\084\084\084\084\084\
-\\084\084\084\084\084\084\084\084\084\084\084\084\084\084\084\000\
-\\000"
+\\084\084\084\084\084\084\084\084\084\084\084\084\084\084\084\084\
+\\084"
 ),
  (84, 
-"\000\000\000\000\000\000\000\000\000\084\000\000\000\000\000\000\
-\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
-\\084\000\000\000\000\000\000\087\084\084\000\084\084\084\084\084\
-\\084\084\084\084\084\084\084\084\084\084\084\084\084\084\084\084\
-\\084\084\084\084\084\084\084\084\084\084\084\084\084\084\084\084\
-\\084\084\084\084\084\084\084\084\084\084\084\084\085\084\084\084\
+"\084\084\084\084\084\084\084\084\084\084\084\084\084\084\084\084\
 \\084\084\084\084\084\084\084\084\084\084\084\084\084\084\084\084\
-\\084\084\084\084\084\084\084\084\084\084\084\084\084\084\084\000\
-\\000"
-),
- (85, 
-"\000\000\000\000\000\000\000\000\000\084\000\000\000\000\000\000\
-\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
-\\084\000\000\000\000\000\000\086\084\084\000\084\084\084\084\084\
+\\084\084\084\084\084\084\084\086\084\084\084\084\084\084\084\084\
 \\084\084\084\084\084\084\084\084\084\084\084\084\084\084\084\084\
 \\084\084\084\084\084\084\084\084\084\084\084\084\084\084\084\084\
 \\084\084\084\084\084\084\084\084\084\084\084\084\085\084\084\084\
 \\084\084\084\084\084\084\084\084\084\084\084\084\084\084\084\084\
-\\084\084\084\084\084\084\084\084\084\084\084\084\084\084\084\000\
+\\084\084\084\084\084\084\084\084\084\084\084\084\084\084\084\084\
+\\084"
+),
+ (85, 
+"\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
+\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
+\\000\000\000\000\000\000\000\084\000\000\000\000\000\000\000\000\
+\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
+\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
+\\000\000\000\000\000\000\000\000\000\000\000\000\084\000\000\000\
+\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
+\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
 \\000"
 ),
+ (89, 
+"\089\089\089\089\089\089\089\089\089\089\000\089\089\089\089\089\
+\\089\089\089\089\089\089\089\089\089\089\089\089\089\089\089\089\
+\\089\089\089\089\089\100\089\089\089\089\089\089\089\089\089\090\
+\\089\089\089\089\089\089\089\089\089\089\089\089\089\089\089\089\
+\\089\089\089\089\089\089\089\089\089\089\089\089\089\089\089\089\
+\\089\089\089\089\089\089\089\089\089\089\089\089\089\089\089\089\
+\\089\089\089\089\089\089\089\089\089\089\089\089\089\089\089\089\
+\\089\089\089\089\089\089\089\089\089\089\089\089\089\089\089\089\
+\\089"
+),
  (90, 
-"\090\090\090\090\090\090\090\090\090\090\000\090\090\090\090\090\
-\\090\090\090\090\090\090\090\090\090\090\090\090\090\090\090\090\
-\\090\090\090\090\090\101\090\090\090\090\090\090\090\090\090\091\
-\\090\090\090\090\090\090\090\090\090\090\090\090\090\090\090\090\
-\\090\090\090\090\090\090\090\090\090\090\090\090\090\090\090\090\
-\\090\090\090\090\090\090\090\090\090\090\090\090\090\090\090\090\
-\\090\090\090\090\090\090\090\090\090\090\090\090\090\090\090\090\
-\\090\090\090\090\090\090\090\090\090\090\090\090\090\090\090\090\
-\\090"
+"\089\089\089\089\089\089\089\089\089\089\000\089\089\089\089\089\
+\\089\089\089\089\089\089\089\089\089\089\089\089\089\089\089\089\
+\\089\089\089\089\089\100\089\089\089\089\091\089\089\089\089\090\
+\\089\089\089\089\089\089\089\089\089\089\089\089\089\089\089\089\
+\\089\089\089\089\089\089\089\089\089\089\089\089\089\089\089\089\
+\\089\089\089\089\089\089\089\089\089\089\089\089\089\089\089\089\
+\\089\089\089\089\089\089\089\089\089\089\089\089\089\089\089\089\
+\\089\089\089\089\089\089\089\089\089\089\089\089\089\089\089\089\
+\\089"
 ),
  (91, 
-"\090\090\090\090\090\090\090\090\090\090\000\090\090\090\090\090\
-\\090\090\090\090\090\090\090\090\090\090\090\090\090\090\090\090\
-\\090\090\090\090\090\101\090\090\090\090\092\090\090\090\090\091\
-\\090\090\090\090\090\090\090\090\090\090\090\090\090\090\090\090\
-\\090\090\090\090\090\090\090\090\090\090\090\090\090\090\090\090\
-\\090\090\090\090\090\090\090\090\090\090\090\090\090\090\090\090\
-\\090\090\090\090\090\090\090\090\090\090\090\090\090\090\090\090\
-\\090\090\090\090\090\090\090\090\090\090\090\090\090\090\090\090\
-\\090"
+"\091\091\091\091\091\091\091\091\091\091\062\091\091\091\091\091\
+\\091\091\091\091\091\091\091\091\091\091\091\091\091\091\091\091\
+\\091\091\091\091\091\095\091\091\091\091\094\091\091\091\091\092\
+\\091\091\091\091\091\091\091\091\091\091\091\091\091\091\091\091\
+\\091\091\091\091\091\091\091\091\091\091\091\091\091\091\091\091\
+\\091\091\091\091\091\091\091\091\091\091\091\091\091\091\091\091\
+\\091\091\091\091\091\091\091\091\091\091\091\091\091\091\091\091\
+\\091\091\091\091\091\091\091\091\091\091\091\091\091\091\091\091\
+\\091"
 ),
  (92, 
-"\092\092\092\092\092\092\092\092\092\092\062\092\092\092\092\092\
-\\092\092\092\092\092\092\092\092\092\092\092\092\092\092\092\092\
-\\092\092\092\092\092\096\092\092\092\092\095\092\092\092\092\093\
-\\092\092\092\092\092\092\092\092\092\092\092\092\092\092\092\092\
-\\092\092\092\092\092\092\092\092\092\092\092\092\092\092\092\092\
-\\092\092\092\092\092\092\092\092\092\092\092\092\092\092\092\092\
-\\092\092\092\092\092\092\092\092\092\092\092\092\092\092\092\092\
-\\092\092\092\092\092\092\092\092\092\092\092\092\092\092\092\092\
-\\092"
+"\091\091\091\091\091\091\091\091\091\091\062\091\091\091\091\091\
+\\091\091\091\091\091\091\091\091\091\091\091\091\091\091\091\091\
+\\091\091\091\091\091\095\091\091\091\091\093\091\091\091\091\092\
+\\091\091\091\091\091\091\091\091\091\091\091\091\091\091\091\091\
+\\091\091\091\091\091\091\091\091\091\091\091\091\091\091\091\091\
+\\091\091\091\091\091\091\091\091\091\091\091\091\091\091\091\091\
+\\091\091\091\091\091\091\091\091\091\091\091\091\091\091\091\091\
+\\091\091\091\091\091\091\091\091\091\091\091\091\091\091\091\091\
+\\091"
 ),
- (93, 
-"\092\092\092\092\092\092\092\092\092\092\062\092\092\092\092\092\
-\\092\092\092\092\092\092\092\092\092\092\092\092\092\092\092\092\
-\\092\092\092\092\092\096\092\092\092\092\094\092\092\092\092\093\
-\\092\092\092\092\092\092\092\092\092\092\092\092\092\092\092\092\
-\\092\092\092\092\092\092\092\092\092\092\092\092\092\092\092\092\
-\\092\092\092\092\092\092\092\092\092\092\092\092\092\092\092\092\
-\\092\092\092\092\092\092\092\092\092\092\092\092\092\092\092\092\
-\\092\092\092\092\092\092\092\092\092\092\092\092\092\092\092\092\
-\\092"
+ (94, 
+"\091\091\091\091\091\091\091\091\091\091\062\091\091\091\091\091\
+\\091\091\091\091\091\091\091\091\091\091\091\091\091\091\091\091\
+\\091\091\091\091\091\095\091\091\091\091\094\091\091\091\091\090\
+\\091\091\091\091\091\091\091\091\091\091\091\091\091\091\091\091\
+\\091\091\091\091\091\091\091\091\091\091\091\091\091\091\091\091\
+\\091\091\091\091\091\091\091\091\091\091\091\091\091\091\091\091\
+\\091\091\091\091\091\091\091\091\091\091\091\091\091\091\091\091\
+\\091\091\091\091\091\091\091\091\091\091\091\091\091\091\091\091\
+\\091"
 ),
  (95, 
-"\092\092\092\092\092\092\092\092\092\092\062\092\092\092\092\092\
-\\092\092\092\092\092\092\092\092\092\092\092\092\092\092\092\092\
-\\092\092\092\092\092\096\092\092\092\092\095\092\092\092\092\091\
-\\092\092\092\092\092\092\092\092\092\092\092\092\092\092\092\092\
-\\092\092\092\092\092\092\092\092\092\092\092\092\092\092\092\092\
-\\092\092\092\092\092\092\092\092\092\092\092\092\092\092\092\092\
-\\092\092\092\092\092\092\092\092\092\092\092\092\092\092\092\092\
-\\092\092\092\092\092\092\092\092\092\092\092\092\092\092\092\092\
-\\092"
+"\095\095\095\095\095\095\095\095\095\095\062\095\095\095\095\095\
+\\095\095\095\095\095\095\095\095\095\095\095\095\095\095\095\095\
+\\095\095\095\095\095\095\095\095\095\095\098\095\095\095\095\096\
+\\095\095\095\095\095\095\095\095\095\095\095\095\095\095\095\095\
+\\095\095\095\095\095\095\095\095\095\095\095\095\095\095\095\095\
+\\095\095\095\095\095\095\095\095\095\095\095\095\095\095\095\095\
+\\095\095\095\095\095\095\095\095\095\095\095\095\095\095\095\095\
+\\095\095\095\095\095\095\095\095\095\095\095\095\095\095\095\095\
+\\095"
 ),
  (96, 
-"\096\096\096\096\096\096\096\096\096\096\062\096\096\096\096\096\
-\\096\096\096\096\096\096\096\096\096\096\096\096\096\096\096\096\
-\\096\096\096\096\096\096\096\096\096\096\099\096\096\096\096\097\
-\\096\096\096\096\096\096\096\096\096\096\096\096\096\096\096\096\
-\\096\096\096\096\096\096\096\096\096\096\096\096\096\096\096\096\
-\\096\096\096\096\096\096\096\096\096\096\096\096\096\096\096\096\
-\\096\096\096\096\096\096\096\096\096\096\096\096\096\096\096\096\
-\\096\096\096\096\096\096\096\096\096\096\096\096\096\096\096\096\
-\\096"
+"\095\095\095\095\095\095\095\095\095\095\062\095\095\095\095\095\
+\\095\095\095\095\095\095\095\095\095\095\095\095\095\095\095\095\
+\\095\095\095\095\095\095\095\095\095\095\097\095\095\095\095\096\
+\\095\095\095\095\095\095\095\095\095\095\095\095\095\095\095\095\
+\\095\095\095\095\095\095\095\095\095\095\095\095\095\095\095\095\
+\\095\095\095\095\095\095\095\095\095\095\095\095\095\095\095\095\
+\\095\095\095\095\095\095\095\095\095\095\095\095\095\095\095\095\
+\\095\095\095\095\095\095\095\095\095\095\095\095\095\095\095\095\
+\\095"
 ),
- (97, 
-"\096\096\096\096\096\096\096\096\096\096\062\096\096\096\096\096\
-\\096\096\096\096\096\096\096\096\096\096\096\096\096\096\096\096\
-\\096\096\096\096\096\096\096\096\096\096\098\096\096\096\096\097\
-\\096\096\096\096\096\096\096\096\096\096\096\096\096\096\096\096\
-\\096\096\096\096\096\096\096\096\096\096\096\096\096\096\096\096\
-\\096\096\096\096\096\096\096\096\096\096\096\096\096\096\096\096\
-\\096\096\096\096\096\096\096\096\096\096\096\096\096\096\096\096\
-\\096\096\096\096\096\096\096\096\096\096\096\096\096\096\096\096\
-\\096"
+ (98, 
+"\095\095\095\095\095\095\095\095\095\095\062\095\095\095\095\095\
+\\095\095\095\095\095\095\095\095\095\095\095\095\095\095\095\095\
+\\095\095\095\095\095\095\095\095\095\095\098\095\095\095\095\099\
+\\095\095\095\095\095\095\095\095\095\095\095\095\095\095\095\095\
+\\095\095\095\095\095\095\095\095\095\095\095\095\095\095\095\095\
+\\095\095\095\095\095\095\095\095\095\095\095\095\095\095\095\095\
+\\095\095\095\095\095\095\095\095\095\095\095\095\095\095\095\095\
+\\095\095\095\095\095\095\095\095\095\095\095\095\095\095\095\095\
+\\095"
 ),
  (99, 
-"\096\096\096\096\096\096\096\096\096\096\062\096\096\096\096\096\
-\\096\096\096\096\096\096\096\096\096\096\096\096\096\096\096\096\
-\\096\096\096\096\096\096\096\096\096\096\099\096\096\096\096\100\
-\\096\096\096\096\096\096\096\096\096\096\096\096\096\096\096\096\
-\\096\096\096\096\096\096\096\096\096\096\096\096\096\096\096\096\
-\\096\096\096\096\096\096\096\096\096\096\096\096\096\096\096\096\
-\\096\096\096\096\096\096\096\096\096\096\096\096\096\096\096\096\
-\\096\096\096\096\096\096\096\096\096\096\096\096\096\096\096\096\
-\\096"
+"\100\100\100\100\100\100\100\100\100\100\000\100\100\100\100\100\
+\\100\100\100\100\100\100\100\100\100\100\100\100\100\100\100\100\
+\\100\100\100\100\100\100\100\100\100\100\095\100\100\100\100\099\
+\\100\100\100\100\100\100\100\100\100\100\100\100\100\100\100\100\
+\\100\100\100\100\100\100\100\100\100\100\100\100\100\100\100\100\
+\\100\100\100\100\100\100\100\100\100\100\100\100\100\100\100\100\
+\\100\100\100\100\100\100\100\100\100\100\100\100\100\100\100\100\
+\\100\100\100\100\100\100\100\100\100\100\100\100\100\100\100\100\
+\\100"
 ),
  (100, 
-"\101\101\101\101\101\101\101\101\101\101\000\101\101\101\101\101\
-\\101\101\101\101\101\101\101\101\101\101\101\101\101\101\101\101\
-\\101\101\101\101\101\101\101\101\101\101\096\101\101\101\101\100\
-\\101\101\101\101\101\101\101\101\101\101\101\101\101\101\101\101\
-\\101\101\101\101\101\101\101\101\101\101\101\101\101\101\101\101\
-\\101\101\101\101\101\101\101\101\101\101\101\101\101\101\101\101\
-\\101\101\101\101\101\101\101\101\101\101\101\101\101\101\101\101\
-\\101\101\101\101\101\101\101\101\101\101\101\101\101\101\101\101\
-\\101"
+"\100\100\100\100\100\100\100\100\100\100\000\100\100\100\100\100\
+\\100\100\100\100\100\100\100\100\100\100\100\100\100\100\100\100\
+\\100\100\100\100\100\100\100\100\100\100\100\100\100\100\100\099\
+\\100\100\100\100\100\100\100\100\100\100\100\100\100\100\100\100\
+\\100\100\100\100\100\100\100\100\100\100\100\100\100\100\100\100\
+\\100\100\100\100\100\100\100\100\100\100\100\100\100\100\100\100\
+\\100\100\100\100\100\100\100\100\100\100\100\100\100\100\100\100\
+\\100\100\100\100\100\100\100\100\100\100\100\100\100\100\100\100\
+\\100"
 ),
  (101, 
-"\101\101\101\101\101\101\101\101\101\101\000\101\101\101\101\101\
-\\101\101\101\101\101\101\101\101\101\101\101\101\101\101\101\101\
-\\101\101\101\101\101\101\101\101\101\101\101\101\101\101\101\100\
-\\101\101\101\101\101\101\101\101\101\101\101\101\101\101\101\101\
-\\101\101\101\101\101\101\101\101\101\101\101\101\101\101\101\101\
-\\101\101\101\101\101\101\101\101\101\101\101\101\101\101\101\101\
-\\101\101\101\101\101\101\101\101\101\101\101\101\101\101\101\101\
-\\101\101\101\101\101\101\101\101\101\101\101\101\101\101\101\101\
-\\101"
+"\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
+\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
+\\000\000\000\000\131\000\000\000\000\000\000\000\000\000\000\000\
+\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
+\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
+\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
+\\000\102\102\128\102\102\124\102\102\118\102\102\108\102\102\102\
+\\102\102\102\102\103\102\102\102\102\102\102\000\000\000\000\000\
+\\000"
 ),
  (102, 
 "\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
 \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
-\\000\000\000\000\132\000\000\000\000\000\000\000\000\000\000\000\
-\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
-\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
-\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
-\\000\103\103\129\103\103\125\103\103\119\103\103\109\103\103\103\
-\\103\103\103\103\104\103\103\103\103\103\103\000\000\000\000\000\
+\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
+\\102\102\102\102\102\102\102\102\102\102\000\000\000\000\000\000\
+\\000\102\102\102\102\102\102\102\102\102\102\102\102\102\102\102\
+\\102\102\102\102\102\102\102\102\102\102\102\000\000\000\000\102\
+\\000\102\102\102\102\102\102\102\102\102\102\102\102\102\102\102\
+\\102\102\102\102\102\102\102\102\102\102\102\000\000\000\000\000\
 \\000"
 ),
  (103, 
 "\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
 \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
 \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
-\\103\103\103\103\103\103\103\103\103\103\000\000\000\000\000\000\
-\\000\103\103\103\103\103\103\103\103\103\103\103\103\103\103\103\
-\\103\103\103\103\103\103\103\103\103\103\103\000\000\000\000\103\
-\\000\103\103\103\103\103\103\103\103\103\103\103\103\103\103\103\
-\\103\103\103\103\103\103\103\103\103\103\103\000\000\000\000\000\
+\\102\102\102\102\102\102\102\102\102\102\000\000\000\000\000\000\
+\\000\102\102\102\102\102\102\102\102\102\102\102\102\102\102\102\
+\\102\102\102\102\102\102\102\102\102\102\102\000\000\000\000\102\
+\\000\102\102\102\102\102\106\102\104\102\102\102\102\102\102\102\
+\\102\102\102\102\102\102\102\102\102\102\102\000\000\000\000\000\
 \\000"
 ),
  (104, 
 "\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
 \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
 \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
-\\103\103\103\103\103\103\103\103\103\103\000\000\000\000\000\000\
-\\000\103\103\103\103\103\103\103\103\103\103\103\103\103\103\103\
-\\103\103\103\103\103\103\103\103\103\103\103\000\000\000\000\103\
-\\000\103\103\103\103\103\107\103\105\103\103\103\103\103\103\103\
-\\103\103\103\103\103\103\103\103\103\103\103\000\000\000\000\000\
+\\102\102\102\102\102\102\102\102\102\102\000\000\000\000\000\000\
+\\000\102\102\102\102\102\102\102\102\102\102\102\102\102\102\102\
+\\102\102\102\102\102\102\102\102\102\102\102\000\000\000\000\102\
+\\000\102\102\102\102\102\105\102\102\102\102\102\102\102\102\102\
+\\102\102\102\102\102\102\102\102\102\102\102\000\000\000\000\000\
 \\000"
 ),
- (105, 
+ (106, 
 "\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
 \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
 \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
-\\103\103\103\103\103\103\103\103\103\103\000\000\000\000\000\000\
-\\000\103\103\103\103\103\103\103\103\103\103\103\103\103\103\103\
-\\103\103\103\103\103\103\103\103\103\103\103\000\000\000\000\103\
-\\000\103\103\103\103\103\106\103\103\103\103\103\103\103\103\103\
-\\103\103\103\103\103\103\103\103\103\103\103\000\000\000\000\000\
+\\102\102\102\102\102\102\102\102\102\102\000\000\000\000\000\000\
+\\000\102\102\102\102\102\102\102\102\102\102\102\102\102\102\102\
+\\102\102\102\102\102\102\102\102\102\102\102\000\000\000\000\102\
+\\000\102\102\102\102\102\107\102\102\102\102\102\102\102\102\102\
+\\102\102\102\102\102\102\102\102\102\102\102\000\000\000\000\000\
 \\000"
 ),
- (107, 
+ (108, 
 "\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
 \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
 \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
-\\103\103\103\103\103\103\103\103\103\103\000\000\000\000\000\000\
-\\000\103\103\103\103\103\103\103\103\103\103\103\103\103\103\103\
-\\103\103\103\103\103\103\103\103\103\103\103\000\000\000\000\103\
-\\000\103\103\103\103\103\108\103\103\103\103\103\103\103\103\103\
-\\103\103\103\103\103\103\103\103\103\103\103\000\000\000\000\000\
+\\102\102\102\102\102\102\102\102\102\102\000\000\000\000\000\000\
+\\000\102\102\102\102\102\102\102\102\102\102\102\102\102\102\102\
+\\102\102\102\102\102\102\102\102\102\102\102\000\000\000\000\102\
+\\000\102\102\102\102\109\102\102\102\102\102\102\102\102\102\102\
+\\102\102\102\102\102\102\102\102\102\102\102\000\000\000\000\000\
 \\000"
 ),
  (109, 
 "\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
 \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
 \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
-\\103\103\103\103\103\103\103\103\103\103\000\000\000\000\000\000\
-\\000\103\103\103\103\103\103\103\103\103\103\103\103\103\103\103\
-\\103\103\103\103\103\103\103\103\103\103\103\000\000\000\000\103\
-\\000\103\103\103\103\110\103\103\103\103\103\103\103\103\103\103\
-\\103\103\103\103\103\103\103\103\103\103\103\000\000\000\000\000\
+\\102\102\102\102\102\102\102\102\102\102\000\000\000\000\000\000\
+\\000\102\102\102\102\102\102\102\102\102\102\102\102\102\102\102\
+\\102\102\102\102\102\102\102\102\102\102\102\000\000\000\000\102\
+\\000\102\102\102\102\102\102\102\102\102\102\102\102\102\102\102\
+\\102\102\102\102\110\102\102\102\102\102\102\000\000\000\000\000\
 \\000"
 ),
  (110, 
 "\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
 \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
 \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
-\\103\103\103\103\103\103\103\103\103\103\000\000\000\000\000\000\
-\\000\103\103\103\103\103\103\103\103\103\103\103\103\103\103\103\
-\\103\103\103\103\103\103\103\103\103\103\103\000\000\000\000\103\
-\\000\103\103\103\103\103\103\103\103\103\103\103\103\103\103\103\
-\\103\103\103\103\111\103\103\103\103\103\103\000\000\000\000\000\
+\\102\102\102\102\102\102\102\102\102\102\000\000\000\000\000\000\
+\\000\102\102\102\102\102\102\102\102\102\102\102\102\102\102\102\
+\\102\102\102\102\102\102\102\102\102\102\102\000\000\000\000\111\
+\\000\102\102\102\102\102\102\102\102\102\102\102\102\102\102\102\
+\\102\102\102\102\102\102\102\102\102\102\102\000\000\000\000\000\
 \\000"
 ),
  (111, 
 "\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
 \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
 \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
-\\103\103\103\103\103\103\103\103\103\103\000\000\000\000\000\000\
-\\000\103\103\103\103\103\103\103\103\103\103\103\103\103\103\103\
-\\103\103\103\103\103\103\103\103\103\103\103\000\000\000\000\112\
-\\000\103\103\103\103\103\103\103\103\103\103\103\103\103\103\103\
-\\103\103\103\103\103\103\103\103\103\103\103\000\000\000\000\000\
+\\102\102\102\102\102\102\102\102\102\102\000\000\000\000\000\000\
+\\000\102\102\102\102\102\102\102\102\102\102\102\102\102\102\102\
+\\102\102\102\102\102\102\102\102\102\102\102\000\000\000\000\102\
+\\000\102\102\102\102\102\115\102\102\102\102\102\102\102\102\102\
+\\102\102\102\102\112\102\102\102\102\102\102\000\000\000\000\000\
 \\000"
 ),
  (112, 
 "\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
 \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
 \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
-\\103\103\103\103\103\103\103\103\103\103\000\000\000\000\000\000\
-\\000\103\103\103\103\103\103\103\103\103\103\103\103\103\103\103\
-\\103\103\103\103\103\103\103\103\103\103\103\000\000\000\000\103\
-\\000\103\103\103\103\103\116\103\103\103\103\103\103\103\103\103\
-\\103\103\103\103\113\103\103\103\103\103\103\000\000\000\000\000\
+\\102\102\102\102\102\102\102\102\102\102\000\000\000\000\000\000\
+\\000\102\102\102\102\102\102\102\102\102\102\102\102\102\102\102\
+\\102\102\102\102\102\102\102\102\102\102\102\000\000\000\000\102\
+\\000\102\102\102\102\102\114\102\102\102\102\102\102\102\102\102\
+\\102\102\102\102\113\102\102\102\102\102\102\000\000\000\000\000\
 \\000"
 ),
- (113, 
+ (115, 
 "\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
 \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
 \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
-\\103\103\103\103\103\103\103\103\103\103\000\000\000\000\000\000\
-\\000\103\103\103\103\103\103\103\103\103\103\103\103\103\103\103\
-\\103\103\103\103\103\103\103\103\103\103\103\000\000\000\000\103\
-\\000\103\103\103\103\103\115\103\103\103\103\103\103\103\103\103\
-\\103\103\103\103\114\103\103\103\103\103\103\000\000\000\000\000\
+\\102\102\102\102\102\102\102\102\102\102\000\000\000\000\000\000\
+\\000\102\102\102\102\102\102\102\102\102\102\102\102\102\102\102\
+\\102\102\102\102\102\102\102\102\102\102\102\000\000\000\000\102\
+\\000\102\102\102\102\102\117\102\102\102\102\102\102\102\102\102\
+\\102\102\102\102\116\102\102\102\102\102\102\000\000\000\000\000\
 \\000"
 ),
- (116, 
+ (118, 
 "\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
 \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
 \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
-\\103\103\103\103\103\103\103\103\103\103\000\000\000\000\000\000\
-\\000\103\103\103\103\103\103\103\103\103\103\103\103\103\103\103\
-\\103\103\103\103\103\103\103\103\103\103\103\000\000\000\000\103\
-\\000\103\103\103\103\103\118\103\103\103\103\103\103\103\103\103\
-\\103\103\103\103\117\103\103\103\103\103\103\000\000\000\000\000\
+\\102\102\102\102\102\102\102\102\102\102\000\000\000\000\000\000\
+\\000\102\102\102\102\102\102\102\102\102\102\102\102\102\102\102\
+\\102\102\102\102\102\102\102\102\102\102\102\000\000\000\000\102\
+\\000\102\102\102\102\102\102\102\102\102\102\102\102\102\102\102\
+\\102\102\102\102\119\102\102\102\102\102\102\000\000\000\000\000\
 \\000"
 ),
  (119, 
 "\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
 \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
 \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
-\\103\103\103\103\103\103\103\103\103\103\000\000\000\000\000\000\
-\\000\103\103\103\103\103\103\103\103\103\103\103\103\103\103\103\
-\\103\103\103\103\103\103\103\103\103\103\103\000\000\000\000\103\
-\\000\103\103\103\103\103\103\103\103\103\103\103\103\103\103\103\
-\\103\103\103\103\120\103\103\103\103\103\103\000\000\000\000\000\
+\\102\102\102\102\102\102\102\102\102\102\000\000\000\000\000\000\
+\\000\102\102\102\102\102\102\102\102\102\102\102\102\102\102\102\
+\\102\102\102\102\102\102\102\102\102\102\102\000\000\000\000\102\
+\\000\102\102\102\102\120\102\102\102\102\102\102\102\102\102\102\
+\\102\102\102\102\102\102\102\102\102\102\102\000\000\000\000\000\
 \\000"
 ),
  (120, 
 "\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
 \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
 \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
-\\103\103\103\103\103\103\103\103\103\103\000\000\000\000\000\000\
-\\000\103\103\103\103\103\103\103\103\103\103\103\103\103\103\103\
-\\103\103\103\103\103\103\103\103\103\103\103\000\000\000\000\103\
-\\000\103\103\103\103\121\103\103\103\103\103\103\103\103\103\103\
-\\103\103\103\103\103\103\103\103\103\103\103\000\000\000\000\000\
+\\102\102\102\102\102\102\102\102\102\102\000\000\000\000\000\000\
+\\000\102\102\102\102\102\102\102\102\102\102\102\102\102\102\102\
+\\102\102\102\102\102\102\102\102\102\102\102\000\000\000\000\121\
+\\000\102\102\102\102\102\102\102\102\102\102\102\102\102\102\102\
+\\102\102\102\102\102\102\102\102\102\102\102\000\000\000\000\000\
 \\000"
 ),
  (121, 
 "\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
 \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
 \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
-\\103\103\103\103\103\103\103\103\103\103\000\000\000\000\000\000\
-\\000\103\103\103\103\103\103\103\103\103\103\103\103\103\103\103\
-\\103\103\103\103\103\103\103\103\103\103\103\000\000\000\000\122\
-\\000\103\103\103\103\103\103\103\103\103\103\103\103\103\103\103\
-\\103\103\103\103\103\103\103\103\103\103\103\000\000\000\000\000\
+\\102\102\102\102\102\102\102\102\102\102\000\000\000\000\000\000\
+\\000\102\102\102\102\102\102\102\102\102\102\102\102\102\102\102\
+\\102\102\102\102\102\102\102\102\102\102\102\000\000\000\000\102\
+\\000\102\102\102\102\102\123\102\102\102\102\102\102\102\102\102\
+\\102\102\102\102\122\102\102\102\102\102\102\000\000\000\000\000\
 \\000"
 ),
- (122, 
+ (124, 
 "\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
 \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
 \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
-\\103\103\103\103\103\103\103\103\103\103\000\000\000\000\000\000\
-\\000\103\103\103\103\103\103\103\103\103\103\103\103\103\103\103\
-\\103\103\103\103\103\103\103\103\103\103\103\000\000\000\000\103\
-\\000\103\103\103\103\103\124\103\103\103\103\103\103\103\103\103\
-\\103\103\103\103\123\103\103\103\103\103\103\000\000\000\000\000\
+\\102\102\102\102\102\102\102\102\102\102\000\000\000\000\000\000\
+\\000\102\102\102\102\102\102\102\102\102\102\102\102\102\102\102\
+\\102\102\102\102\102\102\102\102\102\102\102\000\000\000\000\102\
+\\000\102\102\102\102\102\102\102\102\102\102\102\102\102\102\125\
+\\102\102\102\102\102\102\102\102\102\102\102\000\000\000\000\000\
 \\000"
 ),
  (125, 
 "\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
 \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
 \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
-\\103\103\103\103\103\103\103\103\103\103\000\000\000\000\000\000\
-\\000\103\103\103\103\103\103\103\103\103\103\103\103\103\103\103\
-\\103\103\103\103\103\103\103\103\103\103\103\000\000\000\000\103\
-\\000\103\103\103\103\103\103\103\103\103\103\103\103\103\103\126\
-\\103\103\103\103\103\103\103\103\103\103\103\000\000\000\000\000\
+\\102\102\102\102\102\102\102\102\102\102\000\000\000\000\000\000\
+\\000\102\102\102\102\102\102\102\102\102\102\102\102\102\102\102\
+\\102\102\102\102\102\102\102\102\102\102\102\000\000\000\000\102\
+\\000\102\102\102\102\102\127\102\102\102\102\102\102\102\102\102\
+\\102\102\102\102\126\102\102\102\102\102\102\000\000\000\000\000\
 \\000"
 ),
- (126, 
+ (128, 
 "\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
 \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
 \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
-\\103\103\103\103\103\103\103\103\103\103\000\000\000\000\000\000\
-\\000\103\103\103\103\103\103\103\103\103\103\103\103\103\103\103\
-\\103\103\103\103\103\103\103\103\103\103\103\000\000\000\000\103\
-\\000\103\103\103\103\103\128\103\103\103\103\103\103\103\103\103\
-\\103\103\103\103\127\103\103\103\103\103\103\000\000\000\000\000\
+\\102\102\102\102\102\102\102\102\102\102\000\000\000\000\000\000\
+\\000\102\102\102\102\102\102\102\102\102\102\102\102\102\102\102\
+\\102\102\102\102\102\102\102\102\102\102\102\000\000\000\000\102\
+\\000\102\102\102\102\102\102\102\102\102\102\102\102\102\129\102\
+\\102\102\102\102\102\102\102\102\102\102\102\000\000\000\000\000\
 \\000"
 ),
  (129, 
 "\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
 \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
 \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
-\\103\103\103\103\103\103\103\103\103\103\000\000\000\000\000\000\
-\\000\103\103\103\103\103\103\103\103\103\103\103\103\103\103\103\
-\\103\103\103\103\103\103\103\103\103\103\103\000\000\000\000\103\
-\\000\103\103\103\103\103\103\103\103\103\103\103\103\103\130\103\
-\\103\103\103\103\103\103\103\103\103\103\103\000\000\000\000\000\
+\\102\102\102\102\102\102\102\102\102\102\000\000\000\000\000\000\
+\\000\102\102\102\102\102\102\102\102\102\102\102\102\102\102\102\
+\\102\102\102\102\102\102\102\102\102\102\102\000\000\000\000\102\
+\\000\102\102\102\102\102\130\102\102\102\102\102\102\102\102\102\
+\\102\102\102\102\102\102\102\102\102\102\102\000\000\000\000\000\
 \\000"
 ),
- (130, 
+ (131, 
 "\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
 \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
 \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
-\\103\103\103\103\103\103\103\103\103\103\000\000\000\000\000\000\
-\\000\103\103\103\103\103\103\103\103\103\103\103\103\103\103\103\
-\\103\103\103\103\103\103\103\103\103\103\103\000\000\000\000\103\
-\\000\103\103\103\103\103\131\103\103\103\103\103\103\103\103\103\
-\\103\103\103\103\103\103\103\103\103\103\103\000\000\000\000\000\
+\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
+\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
+\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
+\\000\132\132\132\132\132\132\132\132\132\132\132\132\132\132\132\
+\\132\132\132\132\132\132\132\132\132\132\132\000\000\000\000\000\
 \\000"
 ),
  (132, 
 "\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
 \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
 \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
-\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
-\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
-\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
-\\000\133\133\133\133\133\133\133\133\133\133\133\133\133\133\133\
-\\133\133\133\133\133\133\133\133\133\133\133\000\000\000\000\000\
+\\132\132\132\132\132\132\132\132\132\132\000\000\000\000\000\000\
+\\000\132\132\132\132\132\132\132\132\132\132\132\132\132\132\132\
+\\132\132\132\132\132\132\132\132\132\132\132\000\000\000\000\132\
+\\000\132\132\132\132\132\132\132\132\132\132\132\132\132\132\132\
+\\132\132\132\132\132\132\132\132\132\132\132\000\000\000\000\000\
 \\000"
 ),
  (133, 
-"\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
-\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
-\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
-\\133\133\133\133\133\133\133\133\133\133\000\000\000\000\000\000\
-\\000\133\133\133\133\133\133\133\133\133\133\133\133\133\133\133\
-\\133\133\133\133\133\133\133\133\133\133\133\000\000\000\000\133\
-\\000\133\133\133\133\133\133\133\133\133\133\133\133\133\133\133\
-\\133\133\133\133\133\133\133\133\133\133\133\000\000\000\000\000\
-\\000"
+"\134\134\134\134\134\134\134\134\134\134\134\134\134\134\134\134\
+\\134\134\134\134\134\134\134\134\134\134\134\134\134\134\134\134\
+\\134\134\000\134\134\134\134\134\134\134\134\134\134\134\134\134\
+\\134\134\134\134\134\134\134\134\134\134\134\134\134\134\134\134\
+\\134\134\134\134\134\134\134\134\134\134\134\134\134\134\134\134\
+\\134\134\134\134\134\134\134\134\134\134\134\134\137\134\134\134\
+\\134\134\134\134\134\134\134\134\134\134\134\134\134\134\134\134\
+\\134\134\134\134\134\134\134\134\134\134\134\134\134\134\134\134\
+\\134"
 ),
  (134, 
-"\135\135\135\135\135\135\135\135\135\135\135\135\135\135\135\135\
-\\135\135\135\135\135\135\135\135\135\135\135\135\135\135\135\135\
-\\135\135\000\135\135\135\135\135\135\135\135\135\135\135\135\135\
-\\135\135\135\135\135\135\135\135\135\135\135\135\135\135\135\135\
-\\135\135\135\135\135\135\135\135\135\135\135\135\135\135\135\135\
-\\135\135\135\135\135\135\135\135\135\135\135\135\139\135\135\135\
-\\135\135\135\135\135\135\135\135\135\135\135\135\135\135\135\135\
-\\135\135\135\135\135\135\135\135\135\135\135\135\135\135\135\135\
-\\135"
+"\134\134\134\134\134\134\134\134\134\134\134\134\134\134\134\134\
+\\134\134\134\134\134\134\134\134\134\134\134\134\134\134\134\134\
+\\134\134\136\134\134\134\134\134\134\134\134\134\134\134\134\134\
+\\134\134\134\134\134\134\134\134\134\134\134\134\134\134\134\134\
+\\134\134\134\134\134\134\134\134\134\134\134\134\134\134\134\134\
+\\134\134\134\134\134\134\134\134\134\134\134\134\135\134\134\134\
+\\134\134\134\134\134\134\134\134\134\134\134\134\134\134\134\134\
+\\134\134\134\134\134\134\134\134\134\134\134\134\134\134\134\134\
+\\134"
 ),
  (135, 
-"\135\135\135\135\135\135\135\135\135\135\135\135\135\135\135\135\
-\\135\135\135\135\135\135\135\135\135\135\135\135\135\135\135\135\
-\\135\135\138\135\135\135\135\135\135\135\135\135\135\135\135\135\
-\\135\135\135\135\135\135\135\135\135\135\135\135\135\135\135\135\
-\\135\135\135\135\135\135\135\135\135\135\135\135\135\135\135\135\
-\\135\135\135\135\135\135\135\135\135\135\135\135\136\135\135\135\
-\\135\135\135\135\135\135\135\135\135\135\135\135\135\135\135\135\
-\\135\135\135\135\135\135\135\135\135\135\135\135\135\135\135\135\
-\\135"
+"\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
+\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
+\\000\000\134\000\000\000\000\000\000\000\000\000\000\000\000\000\
+\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
+\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
+\\000\000\000\000\000\000\000\000\000\000\000\000\134\000\000\000\
+\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
+\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
+\\000"
 ),
- (136, 
-"\135\135\135\135\135\135\135\135\135\135\135\135\135\135\135\135\
-\\135\135\135\135\135\135\135\135\135\135\135\135\135\135\135\135\
-\\135\135\137\135\135\135\135\135\135\135\135\135\135\135\135\135\
-\\135\135\135\135\135\135\135\135\135\135\135\135\135\135\135\135\
-\\135\135\135\135\135\135\135\135\135\135\135\135\135\135\135\135\
-\\135\135\135\135\135\135\135\135\135\135\135\135\136\135\135\135\
-\\135\135\135\135\135\135\135\135\135\135\135\135\135\135\135\135\
-\\135\135\135\135\135\135\135\135\135\135\135\135\135\135\135\135\
-\\135"
-),
- (140, 
+ (138, 
 "\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
 \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
-\\000\143\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
-\\000\000\000\000\000\000\000\000\000\000\000\000\000\142\141\000\
+\\000\141\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
+\\000\000\000\000\000\000\000\000\000\000\000\000\000\140\139\000\
 \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
 \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
 \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
 \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
 \\000"
 ),
- (144, 
-"\000\000\000\000\000\000\000\000\000\144\000\000\000\000\000\000\
-\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
-\\144\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
+ (142, 
+"\000\000\000\000\000\000\000\000\000\142\000\000\000\000\000\000\
+\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
+\\142\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
 \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
 \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
 \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
@@ -1130,8 +1130,8 @@
 \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
 \\000"
 ),
- (145, 
-"\000\000\000\000\000\000\000\000\000\000\146\000\000\000\000\000\
+ (143, 
+"\000\000\000\000\000\000\000\000\000\000\144\000\000\000\000\000\
 \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
 \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
 \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
@@ -1156,35 +1156,35 @@
 {fin = [(N 71)], trans = 0},
 {fin = [(N 61)], trans = 0},
 {fin = [(N 86)], trans = 0},
-{fin = [(N 283)], trans = 7},
-{fin = [(N 283)], trans = 8},
-{fin = [(N 283)], trans = 9},
-{fin = [(N 186),(N 283)], trans = 7},
-{fin = [(N 283)], trans = 11},
-{fin = [(N 198),(N 283)], trans = 7},
-{fin = [(N 283)], trans = 13},
-{fin = [(N 283)], trans = 14},
-{fin = [(N 283)], trans = 15},
-{fin = [(N 283)], trans = 16},
-{fin = [(N 283)], trans = 17},
-{fin = [(N 283)], trans = 18},
-{fin = [(N 206),(N 283)], trans = 7},
-{fin = [(N 283)], trans = 20},
-{fin = [(N 283)], trans = 21},
-{fin = [(N 190),(N 283)], trans = 7},
-{fin = [(N 283)], trans = 23},
-{fin = [(N 283)], trans = 24},
-{fin = [(N 194),(N 283)], trans = 7},
+{fin = [(N 271)], trans = 7},
+{fin = [(N 271)], trans = 8},
+{fin = [(N 271)], trans = 9},
+{fin = [(N 174),(N 271)], trans = 7},
+{fin = [(N 271)], trans = 11},
+{fin = [(N 186),(N 271)], trans = 7},
+{fin = [(N 271)], trans = 13},
+{fin = [(N 271)], trans = 14},
+{fin = [(N 271)], trans = 15},
+{fin = [(N 271)], trans = 16},
+{fin = [(N 271)], trans = 17},
+{fin = [(N 271)], trans = 18},
+{fin = [(N 194),(N 271)], trans = 7},
+{fin = [(N 271)], trans = 20},
+{fin = [(N 271)], trans = 21},
+{fin = [(N 178),(N 271)], trans = 7},
+{fin = [(N 271)], trans = 23},
+{fin = [(N 271)], trans = 24},
+{fin = [(N 182),(N 271)], trans = 7},
 {fin = [(N 25)], trans = 0},
 {fin = [(N 80)], trans = 0},
 {fin = [(N 50)], trans = 0},
-{fin = [(N 157)], trans = 29},
+{fin = [(N 145)], trans = 29},
 {fin = [(N 23)], trans = 30},
 {fin = [(N 15)], trans = 0},
 {fin = [(N 12)], trans = 0},
 {fin = [(N 78)], trans = 33},
 {fin = [(N 21)], trans = 0},
-{fin = [(N 315)], trans = 0},
+{fin = [(N 303)], trans = 0},
 {fin = [(N 38)], trans = 0},
 {fin = [(N 31)], trans = 37},
 {fin = [(N 48)], trans = 0},
@@ -1193,10 +1193,10 @@
 {fin = [(N 68)], trans = 0},
 {fin = [(N 41)], trans = 42},
 {fin = [(N 45)], trans = 0},
-{fin = [(N 309)], trans = 0},
+{fin = [(N 297)], trans = 0},
 {fin = [(N 27)], trans = 45},
 {fin = [(N 36)], trans = 0},
-{fin = [(N 318)], trans = 0},
+{fin = [(N 306)], trans = 0},
 {fin = [(N 126)], trans = 48},
 {fin = [], trans = 49},
 {fin = [(N 104)], trans = 49},
@@ -1209,92 +1209,90 @@
 {fin = [], trans = 57},
 {fin = [], trans = 58},
 {fin = [], trans = 59},
-{fin = [(N 182)], trans = 60},
+{fin = [(N 170)], trans = 60},
 {fin = [], trans = 61},
 {fin = [], trans = 62},
 {fin = [], trans = 63},
-{fin = [(N 182)], trans = 64},
-{fin = [(N 182)], trans = 65},
-{fin = [(N 182)], trans = 66},
-{fin = [(N 182)], trans = 67},
-{fin = [(N 182)], trans = 66},
-{fin = [(N 182)], trans = 69},
+{fin = [(N 170)], trans = 64},
+{fin = [(N 170)], trans = 65},
+{fin = [(N 170)], trans = 66},
+{fin = [(N 170)], trans = 67},
+{fin = [(N 170)], trans = 66},
+{fin = [(N 170)], trans = 69},
 {fin = [(N 73)], trans = 70},
 {fin = [(N 130)], trans = 70},
 {fin = [], trans = 72},
 {fin = [(N 55)], trans = 0},
 {fin = [(N 123)], trans = 74},
 {fin = [(N 58)], trans = 75},
-{fin = [(N 306)], trans = 0},
+{fin = [(N 294)], trans = 0},
 {fin = [(N 29)], trans = 0},
-{fin = [(N 300)], trans = 78},
+{fin = [(N 288)], trans = 78},
 {fin = [(N 76)], trans = 0},
-{fin = [(N 302)], trans = 0},
+{fin = [(N 290)], trans = 0},
 {fin = [(N 82)], trans = 0},
 {fin = [(N 52)], trans = 0},
 {fin = [], trans = 83},
 {fin = [], trans = 84},
 {fin = [], trans = 85},
-{fin = [(N 151)], trans = 84},
-{fin = [(N 151)], trans = 0},
+{fin = [(N 139)], trans = 0},
 {fin = [], trans = 85},
 {fin = [(N 9)], trans = 0},
-{fin = [(N 182)], trans = 90},
-{fin = [(N 182)], trans = 91},
-{fin = [(N 182)], trans = 92},
-{fin = [(N 182)], trans = 93},
-{fin = [(N 182)], trans = 92},
-{fin = [(N 182)], trans = 95},
-{fin = [(N 182)], trans = 96},
-{fin = [(N 182)], trans = 97},
-{fin = [(N 182)], trans = 96},
-{fin = [(N 182)], trans = 99},
-{fin = [(N 182)], trans = 100},
-{fin = [(N 182)], trans = 101},
-{fin = [], trans = 102},
-{fin = [(N 290)], trans = 103},
-{fin = [(N 290)], trans = 104},
-{fin = [(N 290)], trans = 105},
-{fin = [(N 211),(N 290)], trans = 103},
-{fin = [(N 290)], trans = 107},
-{fin = [(N 231),(N 290)], trans = 103},
-{fin = [(N 290)], trans = 109},
-{fin = [(N 290)], trans = 110},
-{fin = [(N 290)], trans = 111},
-{fin = [(N 290)], trans = 112},
-{fin = [(N 290)], trans = 113},
-{fin = [(N 277),(N 290)], trans = 103},
-{fin = [(N 253),(N 290)], trans = 103},
-{fin = [(N 290)], trans = 116},
-{fin = [(N 269),(N 290)], trans = 103},
-{fin = [(N 261),(N 290)], trans = 103},
-{fin = [(N 290)], trans = 119},
-{fin = [(N 290)], trans = 120},
-{fin = [(N 290)], trans = 121},
-{fin = [(N 290)], trans = 122},
-{fin = [(N 245),(N 290)], trans = 103},
-{fin = [(N 238),(N 290)], trans = 103},
-{fin = [(N 290)], trans = 125},
-{fin = [(N 290)], trans = 126},
-{fin = [(N 226),(N 290)], trans = 103},
-{fin = [(N 216),(N 290)], trans = 103},
-{fin = [(N 290)], trans = 129},
-{fin = [(N 290)], trans = 130},
-{fin = [(N 221),(N 290)], trans = 103},
-{fin = [], trans = 132},
-{fin = [(N 298)], trans = 133},
+{fin = [(N 170)], trans = 89},
+{fin = [(N 170)], trans = 90},
+{fin = [(N 170)], trans = 91},
+{fin = [(N 170)], trans = 92},
+{fin = [(N 170)], trans = 91},
+{fin = [(N 170)], trans = 94},
+{fin = [(N 170)], trans = 95},
+{fin = [(N 170)], trans = 96},
+{fin = [(N 170)], trans = 95},
+{fin = [(N 170)], trans = 98},
+{fin = [(N 170)], trans = 99},
+{fin = [(N 170)], trans = 100},
+{fin = [], trans = 101},
+{fin = [(N 278)], trans = 102},
+{fin = [(N 278)], trans = 103},
+{fin = [(N 278)], trans = 104},
+{fin = [(N 199),(N 278)], trans = 102},
+{fin = [(N 278)], trans = 106},
+{fin = [(N 219),(N 278)], trans = 102},
+{fin = [(N 278)], trans = 108},
+{fin = [(N 278)], trans = 109},
+{fin = [(N 278)], trans = 110},
+{fin = [(N 278)], trans = 111},
+{fin = [(N 278)], trans = 112},
+{fin = [(N 265),(N 278)], trans = 102},
+{fin = [(N 241),(N 278)], trans = 102},
+{fin = [(N 278)], trans = 115},
+{fin = [(N 257),(N 278)], trans = 102},
+{fin = [(N 249),(N 278)], trans = 102},
+{fin = [(N 278)], trans = 118},
+{fin = [(N 278)], trans = 119},
+{fin = [(N 278)], trans = 120},
+{fin = [(N 278)], trans = 121},
+{fin = [(N 233),(N 278)], trans = 102},
+{fin = [(N 226),(N 278)], trans = 102},
+{fin = [(N 278)], trans = 124},
+{fin = [(N 278)], trans = 125},
+{fin = [(N 214),(N 278)], trans = 102},
+{fin = [(N 204),(N 278)], trans = 102},
+{fin = [(N 278)], trans = 128},
+{fin = [(N 278)], trans = 129},
+{fin = [(N 209),(N 278)], trans = 102},
+{fin = [], trans = 131},
+{fin = [(N 286)], trans = 132},
+{fin = [], trans = 133},
 {fin = [], trans = 134},
 {fin = [], trans = 135},
-{fin = [], trans = 136},
-{fin = [(N 95)], trans = 135},
 {fin = [(N 95)], trans = 0},
-{fin = [], trans = 136},
-{fin = [(N 33)], trans = 140},
-{fin = [(N 312)], trans = 0},
+{fin = [], trans = 135},
+{fin = [(N 33)], trans = 138},
+{fin = [(N 300)], trans = 0},
 {fin = [(N 64)], trans = 0},
 {fin = [(N 18)], trans = 0},
-{fin = [(N 2)], trans = 144},
-{fin = [(N 7)], trans = 145},
+{fin = [(N 2)], trans = 142},
+{fin = [(N 7)], trans = 143},
 {fin = [(N 7)], trans = 0}])
 end
 structure StartStates =
@@ -1343,44 +1341,44 @@
 | 123 => let val yytext=yymktext() in col:=yypos-(!eolpos); T.SIGNED_INTEGER(yytext,!linep,!col) end
 | 126 => let val yytext=yymktext() in col:=yypos-(!eolpos); T.UNSIGNED_INTEGER(yytext,!linep,!col) end
 | 130 => let val yytext=yymktext() in col:=yypos-(!eolpos); T.DOT_DECIMAL(yytext,!linep,!col) end
+| 139 => let val yytext=yymktext() in col:=yypos-(!eolpos); T.SINGLE_QUOTED(yytext,!linep,!col) end
+| 145 => let val yytext=yymktext() in col:=yypos-(!eolpos); T.UPPER_WORD(yytext,!linep,!col) end
 | 15 => (col:=yypos-(!eolpos); T.DEFIN_CHOICE(!linep,!col))
-| 151 => let val yytext=yymktext() in col:=yypos-(!eolpos); T.SINGLE_QUOTED(yytext,!linep,!col) end
-| 157 => let val yytext=yymktext() in col:=yypos-(!eolpos); T.UPPER_WORD(yytext,!linep,!col) end
+| 170 => let val yytext=yymktext() in col:=yypos-(!eolpos); count_commentlines yytext;T.COMMENT(yytext,!linep,!col) end
+| 174 => (col:=yypos-(!eolpos); T.THF(!linep,!col))
+| 178 => (col:=yypos-(!eolpos); T.FOF(!linep,!col))
 | 18 => (col:=yypos-(!eolpos); T.OPERATOR_FORALL(!linep,!col))
-| 182 => let val yytext=yymktext() in col:=yypos-(!eolpos); count_commentlines yytext;T.COMMENT(yytext,!linep,!col) end
-| 186 => (col:=yypos-(!eolpos); T.THF(!linep,!col))
-| 190 => (col:=yypos-(!eolpos); T.FOF(!linep,!col))
-| 194 => (col:=yypos-(!eolpos); T.CNF(!linep,!col))
-| 198 => (col:=yypos-(!eolpos); T.TFF(!linep,!col))
+| 182 => (col:=yypos-(!eolpos); T.CNF(!linep,!col))
+| 186 => (col:=yypos-(!eolpos); T.TFF(!linep,!col))
+| 194 => (col:=yypos-(!eolpos); T.INCLUDE(!linep,!col))
+| 199 => (col:=yypos-(!eolpos); T.DTHF(!linep,!col))
 | 2 => let val yytext=yymktext() in col:=(!col)+size yytext; continue ()  end
-| 206 => (col:=yypos-(!eolpos); T.INCLUDE(!linep,!col))
+| 204 => (col:=yypos-(!eolpos); T.DFOF(!linep,!col))
+| 209 => (col:=yypos-(!eolpos); T.DCNF(!linep,!col))
 | 21 => (col:=yypos-(!eolpos); T.OPERATOR_EXISTS(!linep,!col))
-| 211 => (col:=yypos-(!eolpos); T.DTHF(!linep,!col))
-| 216 => (col:=yypos-(!eolpos); T.DFOF(!linep,!col))
-| 221 => (col:=yypos-(!eolpos); T.DCNF(!linep,!col))
-| 226 => (col:=yypos-(!eolpos); T.DFOT(!linep,!col))
+| 214 => (col:=yypos-(!eolpos); T.DFOT(!linep,!col))
+| 219 => (col:=yypos-(!eolpos); T.DTFF(!linep,!col))
+| 226 => (col:=yypos-(!eolpos); T.ITE_F(!linep,!col))
 | 23 => (col:=yypos-(!eolpos); T.AT_SIGN(!linep,!col))
-| 231 => (col:=yypos-(!eolpos); T.DTFF(!linep,!col))
-| 238 => (col:=yypos-(!eolpos); T.ITE_F(!linep,!col))
-| 245 => (col:=yypos-(!eolpos); T.ITE_T(!linep,!col))
+| 233 => (col:=yypos-(!eolpos); T.ITE_T(!linep,!col))
+| 241 => (col:=yypos-(!eolpos); T.LET_TF(!linep,!col))
+| 249 => (col:=yypos-(!eolpos); T.LET_FF(!linep,!col))
 | 25 => (col:=yypos-(!eolpos); T.CARET(!linep,!col))
-| 253 => (col:=yypos-(!eolpos); T.LET_TF(!linep,!col))
-| 261 => (col:=yypos-(!eolpos); T.LET_FF(!linep,!col))
-| 269 => (col:=yypos-(!eolpos); T.LET_FT(!linep,!col))
+| 257 => (col:=yypos-(!eolpos); T.LET_FT(!linep,!col))
+| 265 => (col:=yypos-(!eolpos); T.LET_TT(!linep,!col))
 | 27 => (col:=yypos-(!eolpos); T.COLON(!linep,!col))
-| 277 => (col:=yypos-(!eolpos); T.LET_TT(!linep,!col))
-| 283 => let val yytext=yymktext() in col:=yypos-(!eolpos); T.LOWER_WORD(yytext,!linep,!col) end
+| 271 => let val yytext=yymktext() in col:=yypos-(!eolpos); T.LOWER_WORD(yytext,!linep,!col) end
+| 278 => let val yytext=yymktext() in col:=yypos-(!eolpos); T.DOLLAR_WORD(yytext,!linep,!col) end
+| 286 => let val yytext=yymktext() in col:=yypos-(!eolpos); T.DOLLAR_DOLLAR_WORD(yytext,!linep,!col) end
+| 288 => (col:=yypos-(!eolpos); T.PLUS(!linep,!col))
 | 29 => (col:=yypos-(!eolpos); T.COMMA(!linep,!col))
-| 290 => let val yytext=yymktext() in col:=yypos-(!eolpos); T.DOLLAR_WORD(yytext,!linep,!col) end
-| 298 => let val yytext=yymktext() in col:=yypos-(!eolpos); T.DOLLAR_DOLLAR_WORD(yytext,!linep,!col) end
-| 300 => (col:=yypos-(!eolpos); T.PLUS(!linep,!col))
-| 302 => (col:=yypos-(!eolpos); T.TIMES(!linep,!col))
-| 306 => (col:=yypos-(!eolpos); T.GENTZEN_ARROW(!linep,!col))
-| 309 => (col:=yypos-(!eolpos); T.SUBTYPE(!linep,!col))
+| 290 => (col:=yypos-(!eolpos); T.TIMES(!linep,!col))
+| 294 => (col:=yypos-(!eolpos); T.GENTZEN_ARROW(!linep,!col))
+| 297 => (col:=yypos-(!eolpos); T.SUBTYPE(!linep,!col))
+| 300 => (col:=yypos-(!eolpos); T.DEP_PROD(!linep,!col))
+| 303 => (col:=yypos-(!eolpos); T.DEP_SUM(!linep,!col))
+| 306 => (col:=yypos-(!eolpos); T.LET_TERM(!linep,!col))
 | 31 => (col:=yypos-(!eolpos); T.EQUALS(!linep,!col))
-| 312 => (col:=yypos-(!eolpos); T.DEP_PROD(!linep,!col))
-| 315 => (col:=yypos-(!eolpos); T.DEP_SUM(!linep,!col))
-| 318 => (col:=yypos-(!eolpos); T.LET_TERM(!linep,!col))
 | 33 => (col:=yypos-(!eolpos); T.EXCLAMATION(!linep,!col))
 | 36 => (col:=yypos-(!eolpos); T.LET(!linep,!col))
 | 38 => (col:=yypos-(!eolpos); T.ARROW(!linep,!col))
@@ -5683,7 +5681,7 @@
 end
 |  ( 276, ( ( _, ( MlyValue.SINGLE_QUOTED SINGLE_QUOTED, 
 SINGLE_QUOTED1left, SINGLE_QUOTED1right)) :: rest671)) => let val  
-result = MlyValue.atomic_word (( SINGLE_QUOTED ))
+result = MlyValue.atomic_word (( dequote SINGLE_QUOTED ))
  in ( LrTable.NT 8, ( result, SINGLE_QUOTED1left, SINGLE_QUOTED1right)
 , rest671)
 end