Hi Thomas, Am 14.01.2014 um 14:43 schrieb Thomas Sewell <[email protected]>:
> 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 _______________________________________________ isabelle-dev mailing list [email protected] https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
