Re: [isabelle] undefined & None
On Tue, 2013-10-01 at 11:18 +0200, Peter Lammich wrote:
> > I am not sure how widespread this usage still is in Isabelle. But where
> > it happens, I consider it a (minor) shortcoming, because it leads to
> > spurious equations: the user arguably never intended to specify that,
> > e.g., "hd  = last ".
> However, this comes in handy in some cases. [...]
Obviously, stronger assumptions allow us to prove stronger theorems. But
the real issue is whether our models are still sound.
This archive was generated by a fusion of
Pipermail (Mailman edition) and