我有一個功能foo，它可以在string類型上工作。當我export_code foo in Scala file -我得到一個非常醜陋的Scala代碼。 一個很長的列表，看起來像這樣創建 abstract sealed class nibble
final case class Nibble0() extends nibble
final case class Nibble1() exten
我們假設我有一個目錄isabelle_afp，其中存儲了很多理論。這個目錄是一個庫，我不打算改變其中的文件。我想加快Isabelle/jEdit的啓動時間（默認情況下，我現在的理論依賴的所有理論都會重新處理）。 如何跳過這一步？ system manual告訴我要構建一個持久堆映像。最簡單的方法是什麼？ 我該如何告訴Isabelle/jEdit加載這個堆映像？
我想在locale內創建一個可執行文件inductive。如果沒有locale一切工作正常： definition "P a b = True"
inductive test :: "'a ⇒ 'a ⇒ bool" where
"test a a" |
"test a b ⟹ P b c ⟹ test a c"
code_pred test .
然而，當我嘗試同樣的
我希望直接從locale定義生成代碼，而不需要解釋。例如： (* A locale, from the code point of view, similar to a class *)
locale MyTest =
fixes L :: "string list"
assumes distinctL: "distinct L"
begin
defini