Re: [isabelle] What is sumC?



> 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.