BEGIN {
  char doublequote;

#   Sorry, but most awk's are not able to deal with double quotes...
  doublequote=34;
  printf("char *dec[]={\n")
  printf("   %cO_NOP%c,\n",doublequote,doublequote)
}
{
  printf("   %c%s%c,\n", doublequote, $1, doublequote)
}
END {
  printf("   %c%c};\n",doublequote,doublequote)
}