試圖瞭解在伊莎貝爾「語法」關鍵字/ HOL

Question

我想了解實施伊莎貝爾/ HOL線性邏輯：https://www.cl.cam.ac.uk/research/hvg/Isabelle/dist/library/Sequents/Sequents/ILL.html對於不syntax關鍵字代表什麼，什麼是代碼的意思是：

syntax 
    "_Trueprop" :: "single_seqe" ("((_)/ ⊢ (_))" [6,6] 5) 
    "_Context" :: "two_seqe" ("((_)/ :=: (_))" [6,6] 5) 
    "_PromAux" :: "three_seqe" ("promaux {_||_||_}") 

我在哪裏可以找到syntax關鍵字的文檔？關於infixr以及計算機科學講義第828卷中的翻譯規則，我找到了詳盡的文檔。但是我找不到關於syntax的類似文檔。

Answer 1

這在參考手冊的8.5.2節（截至2016年1月1日）中描述：「原始語法和翻譯」。

這裏的第一行表示添加語法規則，表示P ⊢ Q解析爲_Trueprop P Q。​​的下一行給出parse_translation，稍後在參考手冊的相同章節中進行描述。該翻譯告訴Isabelle將_Trueprop翻譯爲K (single_tr Trueprop)，並將Trueprop聲明爲文件頂部的未解釋常量。你會看到還有一個print_translation，它控制漂亮的打印機。