如何在Isabelle中输入粗体符号？jEdit符号ASCII查询方法咨询

一、输入粗体*和粗体1符号的方法 #

针对Isabelle代码中使用的粗体运算符（如示例中的❙*和❙1），在jEdit中有两种便捷输入方式：

• 符号命令补全：输入LaTeX风格的命令后按Tab键自动替换为Unicode符号：
  • 输入\boldasterisk并按Tab，得到粗体星号
  • 输入\bold1并按Tab，得到粗体数字1
• Unicode直接输入：按下Ctrl+Shift+U，输入符号的十六进制码点后回车：
  • 粗体星号对应码点1D6C1
  • 粗体数字1对应码点1D7D8

二、查询任意符号的ASCII版本 #

若需获取符号的ASCII兼容写法，可通过以下方式：

• Isabelle符号检查：将光标定位到目标符号上，按下Ctrl+Shift+I，弹出的窗口会显示符号的详细信息，包括对应的ASCII命令或等价替代方案。
• jEdit字符信息工具：选中符号后，打开Utilities菜单选择Character Information，查看字符的编码与别名，从中提取ASCII替代（若存在）。
• Isabelle内置帮助：按下F1打开Isabelle帮助文档，搜索符号名称，即可找到其ASCII兼容的定义方式（例如多数粗体符号可使用普通ASCII字符配合locale的notation声明实现等价功能）。

内容的提问来源于stack exchange，提问作者alagris