Re: [isabelle] Real number numeric literals in Isabelle

-----Original Message-----
From: cl-isabelle-users-bounces at
[mailto:cl-isabelle-users-bounces at] On Behalf Of Norbert
Sent: Friday, December 16, 2005 10:52 AM

>Why do you think this measure is bad?

I do not know if the measure is bad. My problem is actually that I do
not really understand how measure works so it took me sometime to think
of this one...

I was wondering how someone else with experience would use measure on
real numbers. 

>HOL is a logic of total functions. So you cannot just leave out cases.
But since every type in HOL has at least one       >member,  there is
indeed a default value called arbitrary. You can return it instead of
-1, to emphasise that this is a >"dead end"...

Ah ha. I will try this.

>   Norbert



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