如何从伊莎贝尔打印到Latex的类型定义？

Question

我正在使用Isabelle文档准备来生成tex文件。我想知道是否有一个反引号的数据类型定义，以便它将完全打印在胶乳。

在某些文件中有一个定义

datatype t = A nat | B bool

稍后我想把这个定义打印给乳胶。我在伊莎贝尔的医生里找不到怎么做的。

一个反引号@{datatype xyz}是伊莎贝尔邮件列表中的提到过，但它对我不起作用(伊莎贝尔2013-2)。

有人知道类型定义的适当反引号吗？

Answer 1

这似乎适用于我在伊莎贝尔2013-2。

伊莎贝尔理论档案：

theory Baz
imports Main
begin

datatype t = A nat | B bool

text {*
  @{datatype t}
*}

end

文件中的结果：

​

​

第一个datatype是定义，第二个是显示反引号.

也许问题是您的@{datatype}反报价不是在text {* ... *}块中吗？