Re: [isabelle] What is sumC?

The theory Fact was combined with Binomial and is now included in Complex_Main. The integer version of the factorial function no longer exists. See NEWS:

The factorial function, "fact", now has type "nat = 'a" (of sort semiring_char_0, which admits numeric types including nat, int, real and complex. INCOMPATIBILITY: an expression such as "fact 3 = 6" may require a type constraint, and the combination "real (fact k)" is likely to be unsatisfactory. If a type conversion is still necessary, then use "of_nat (fact k)" or "real_of_nat (fact k)”.

Larry Paulson

> On 28 Apr 2015, at 08:21, Lars Hupel <hupel at> wrote:
>> I was importing the one defined in theory Fact, which I got (without
>> defining it myself) from the line "theory Factorial imports Main Fact
>> begin ...":
>> fun
>> fact_nat :: "nat => nat"
>> where
>> fact__nat: "fact_nat 0 = Suc 0"
>> | fact-Suc: "fact_nat (Suc x) = Suc x * fact x"
>> I'm not sure, by the way, why this is called fact_nat in theory Fact,
>> rather than just fact.
> After digging a bit, it turns out that the Fact theory is part of HOL in
> Isabelle2014, but not anymore in Isabelle2015-RC*.
> I couldn't reproduce the tactic failure, though. 'simp add:
> eval_nat_numeral' solves the goal just fine.
> Cheers
> Lars

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