[isabelle] How can I use Code_Abstract_Nat in Isabelle?



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


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.