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
