On 05.06.2014 05:44, Thomas Sewell wrote: > In particular, I want to avoid ever changing the setting globally. I've > had some bad experiences in the past with theories with differing global > configurations, which means that the location of a tactic and the > include graphs of theories start having subtle effects on the way the > tactics run. It's a mess.
A little less invasive would be enabling the compatibility mode for a whole theory using "context notes [[...]] begin ... end".
signature.asc
Description: OpenPGP digital signature
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
