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