On 28/10/16 13:52, Lawrence Paulson wrote: > I hope these won't be deprecated. Even though they are a bit longer, they are > logical and easy to remember (due to the parallels with fix/assume/show). > Larry > >> On 27 Oct 2016, at 22:20, Makarius <makar...@sketis.net> wrote: >> >> Note that the long form with fixes/assumes/shows has become a bit >> old-fashioned, although there is nothing wrong with it apart from being >> too long for short statements. >> >> The new eigen-context notation "theorem B if A for x" often works >> better, but there no print command for that yet. In fact, I would like >> to make the "for x" form standard for almost all output, e.g. plain >> 'thm'. But that is a different story for a different release. >
fixes/assumes/show is not going to disappear; it is required as dual form of fixes/assumes/obtains, which is not covered by the new eigen-context notation. BTW, there is strictly speaking no need to use fix/assume/show, since show if/for is already possible, although relatively rarely used. Makarius _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev