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

[Jasmin Christian Blanchette]

Hi Thomas,

Am 14.01.2014 um 14:43 schrieb Thomas Sewell <Thomas.Sewell at nicta.com.au>:

> To address Jasmin and Larry's concern, it is possible to switch back to the "compatibility mode" by setting a config variable in the context, or by calling the ML version with an extra parameter. Any legacy proof script can be repaired by adding the line "using [[ hypsubst_thin = true ]]" before any apply/by line.

That's perfect.

> I understand why Tjark and Larry would prefer a minimal change, using contextual information to decide when to deviate from the old behaviour. It would certainly create less maintenance work. Let me elaborate why this approach is my first preference:
> [...]
>  2) Having the behaviour of tactics change because of largely invisible background concerns seems a recipe for confusion. This particularly applies to building-block tactics such as safe and clarify. I would prefer they be predictable and reliable.

Yes. While I agree with Tjark in principle, it appears to me that the syntactic conditions you described are weird enough (even though they make sense upon reflection) that they would confuse users, possibly even those who have been following this thread.

Regards,

Jasmin