Hi Rene,
> =
> locale foo = fixes f :: "nat => nat"
> assumes f_mono[termination_simp]: "f x <= x"
> begin
>
> fun bar :: "nat => nat" where
> "bar 0 = 0"
> | "bar (Suc x) = Suc (bar (f x))"
>
> end
>
> definition com where
> [code del]: "com = foo.bar id"
>
> interpretation foo id
Hi Clemens,
>> If one imports HOL-Algebra.Multiplicative_Group (which we actually do
>> via some transitive import), then \mu (LFP), \nu (GFP) and
>> \phi (Euler’s totient function) become constants.
>
> Unless I hear otherwise I will replace \mu by LFP and \nu by GFP.
sorry, I didn't
> Is it intentional that the "Computational_Algebra" theory does not
> import "Polynomial_Factorial"?
Yes. Polynomial_Factorial requires Field_as_Ring, which does a
substantial modification to the type class hierarchy, pulling it apart
from long-established traditions in HOL-Main. I have been
