* The standard proof method of commands 'proof' and '..' is now called
"standard" to make semantically clear what it is; the old name "default"
is still available as legacy for some time. Documentation now explains
'..' more accurately as "by standard" instead of "by rule".
This refers to Isabelle/4c79543cc376, which also contains the updates to
the documentation. I did not make any further changes in the applications,
to give more time to figure out if this is a convincing idea.
Updating old proofs, I've come across slightly odd situations like this:
proof (default, goals)
which would then become this:
proof (standard, goals)
The "standard" wording is from my explanation of Isar 'proof' or '..' in
the past couple of years. The above also resolves the oddity in the
manuals to mix up "by rule" and "by default" in unsystematic ways. The
fine point here is the extra inclusion of "intro_classes" and
"intro_locales" in the standard step, which was formally swept under the
carpet in the past -- as some users have occasionally pointed out.
Makarius
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
