Hello Ramana.
On 05/10/17 19:18, Ramana Kumar wrote:
> My intuition says that working with total functions (and especially
> predicates) will be easier.
> Why? I don't know exactly, but here are some possible reasons:
> you can just use plain rewriting rather than conditional rewriting,
> and you
Hello Jeremy.
Thanks for your reply.
On 05/10/17 13:25, Jeremy Dawson wrote:
> Hi Mario,
>
> I don't mind the question, but the answer may not be much use because
> it's a comparison between the 2005 version of Isabelle which I use and
> HOL4.
>
> In terms of the type systems they are
