[isabelle-dev] Safe approach to hypothesis substitution mark II

[Peter Lammich]

> If there's interest in getting this change installed, I'll slog through these, and then figure out what's broken and what's expected to be broken in the latest tip of Isabelle and in the AFP. I'd call for volunteers to help with that bit though.
> 

I would very much appreciate such a change to hypsubst! (Having thought
of doing this patch myself several times, not knowing about the older
discussion on this list ;) )

--
  Peter



> All comments welcome,
>      Thomas.
> 
> 
> ________________________________
> 
> The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev