Isabelle 中的 (*>*) 是什么？
What is (*>*) in Isabelle?
我在伊莎贝尔下载了几个使用(*<*)和(*>*)的.thy文件。据我所知，它们似乎没有效果，但它们一定有目的.有谁知道它们的用途吗？
特殊注释(*<*)和(*>*)告诉Isabelle的文档准备系统不要在生成的PDF文档中包含所附的理论文本。它们是 %invisible 等结构化标签的前身，这些标签还控制生成的文档中出现的内容。例如，
lemma %invisible silly: "0 = 0" by simp
和
(*<*)
lemma silly: "0 = 0" by simp
(*>*)
效果大致相同，即整个引理及其证明不会出现在文档中。但是，标签只能附加到顶级命令，如 definition、lemma、proof、by。因此，您不能像
那样只隐藏命令的一部分
by(simp add: take_map(*<*) drop_map(*>*))
这将在 PDF 中产生 by(simp add: take_map)，即省略 drop_map。
我在伊莎贝尔下载了几个使用(*<*)和(*>*)的.thy文件。据我所知，它们似乎没有效果，但它们一定有目的.有谁知道它们的用途吗？
特殊注释(*<*)和(*>*)告诉Isabelle的文档准备系统不要在生成的PDF文档中包含所附的理论文本。它们是 %invisible 等结构化标签的前身，这些标签还控制生成的文档中出现的内容。例如，
lemma %invisible silly: "0 = 0" by simp
和
(*<*)
lemma silly: "0 = 0" by simp
(*>*)
效果大致相同，即整个引理及其证明不会出现在文档中。但是，标签只能附加到顶级命令，如 definition、lemma、proof、by。因此，您不能像
by(simp add: take_map(*<*) drop_map(*>*))
这将在 PDF 中产生 by(simp add: take_map)，即省略 drop_map。