That theory should be cleaned up and separated into its core and the
real-related lemmas that are trivial consequences. The real-related
stuff should go where it is used, or better, be removed: eg
real (fact n) = 0
is pointless, at least as a simp rule. Such cleaning up is greatly
appreciated
This ancient development deserves whatever reorganisation you feel is
appropriate.
Larry
On 29 Jan 2009, at 15:42, Amine Chaieb wrote:
> Dear all,
>
> For now HOL/Fact.thy defines factorials (over natural numbers) and
> strangely imports the reals. The theorem involving the reals,
> however
Dear all,
For now HOL/Fact.thy defines factorials (over natural numbers) and
strangely imports the reals. The theorem involving the reals, however,
hold in any (ordered) (ring/field) of charachteristic Zero.
Apart from that, I have a formalization of Pochhammer's symbol (raising
factorials) wh
