Yes, the same here. I would like to use specification sometimes, but without supporting contexts it not as helpful as it could. I also do not need ax_specification.
So my preference is option (b). - Johannes Am Freitag, den 14.03.2014, 15:10 +0100 schrieb Andreas Lochbihler: > I myself found specification quite convenient and use it occasionally, e.g., > in > AFP/Containers/Set_Linorder and a number of my private developments. It's a > useful > shortcut to a definition with SOME and deriving the properties later with > someI. It would > be good if it works with contexts. I have never used ax_specification, though. > > Andreas > > On 14/03/14 14:44, Makarius wrote: > > On Fri, 14 Mar 2014, Jasmin Blanchette wrote: > > > >>> * HOL/Tools/choice_specification.ML which is loaded into > >>> HOL/Hilbert_Choice.thy -- really old stuff that would require serious > >>> renovation if actually used: 'ax_specification' with its unchecked > >>> axiomatization is actually unsed, and 'specification' only by > >>> HOL-Auth (and its many clones). > >>> > >>> A candidate for HOL-Library, after removing the axiomatic part? > >>> Nitpick seems to have special tricks to cope with it, though. > >> > >> These special tricks could be taken out. They're not vital in any way. > > > > (This deserves its own mail thread.) > > > > Motivated by the surprise about ``"code_pred" introduces axioms?'' from > > last October > > https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2013-October/msg00228.html > > I've checked the situation more systematically some weeks ago. > > > > Spurious axiomatizations can lead to unpleasant surprises to users that are > > unaware of the > > danger. We probably can't do anything about code_pred now, but check the > > general > > situations about further such trapdoors. > > > > > > So how about 'ax_specification'? It is an alternate personality of > > 'specification' that > > would make it very hard to renovate the latter, if that is desirable at all: > > 'ax_specification' is unused and 'specification' only used in HOL-Auth and > > its > > derivatives, which appears to have been a demo for that. > > > > There are various possibilities: > > > > (a) Do nothing and let this old stuff collect more dust. > > > > (b) Remove 'ax_specification' and brush-up 'specification' a little > > (proper local contexts, PIDE markup etc.). > > > > (c) Remove both 'ax_specification' and 'specification', and do the > > HOL-Auth applications with a hypothetical context, potentially > > with a proven interpretation of the assumptions. > > > > > > Makarius > > _______________________________________________ > > isabelle-dev mailing list > > [email protected] > > https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev > _______________________________________________ > isabelle-dev mailing list > [email protected] > https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev _______________________________________________ isabelle-dev mailing list [email protected] https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
