I think you really want to import "HOL-Library.Code_Target_Numeral" instead of what you imported. It seems to work with that.
Side note: importing things with "~~/src/HOL/…" is somewhat old-fashioned and can lead to problems. It's not the problem here, but still. Using the session-qualified import (as above) is better.
Hi Michael, which Isabelle release do you use? Currently, there are a couple of RCs for the upcoming release, so this is an important information to investigate your issue. Cheers, Florian Am 19.11.21 um 06:14 schrieb Michael Stampone:I would like to learn how to use function transformers in Isabelle. I tried to make this minimal example and it didn't work, maybe I'm missing something obvious. Please help me get this example to run so I can understand Isabelle better. theory Scratch imports Main "~~/src/HOL/Library/Code_Abstract_Nat" begin primrec f :: "nat ⇒ nat" where "f 0 = 0" | "f (Suc x) = f x" declare [[show_types]] code_thms f I get an error message on the last line which says No content for theory certificate HOL.Nat Eventually, I would like to also export_code f in SML module_name Whatever