* Basic constants of Pure use more conventional names and are always
qualified. Rare INCOMPATIBILITY, but with potentially serious
consequences, notably for tools in Isabelle/ML. The following
renaming needs to be applied:
== ~> Pure.eq
==> ~> Pure.imp
all ~> Pure.all
TYPE ~> Pure.type
dummy_pattern ~> Pure.dummy_pattern
Systematic porting works by using the following theory setup on a
*previous* Isabelle version to introduce the new name accesses for the
old constants:
setup {*
fn thy => thy
|> Sign.root_path
|> Sign.const_alias (Binding.qualify true "Pure" @{binding eq}) "=="
|> Sign.const_alias (Binding.qualify true "Pure" @{binding imp}) "==>"
|> Sign.const_alias (Binding.qualify true "Pure" @{binding all}) "all"
|> Sign.restore_naming thy
*}
Thus ML antiquotations like @{const_name Pure.eq} may be used already.
Later the application is moved to the current Isabelle version, and
the auxiliary aliases are deleted.
This refers to Isabelle/84fc7dfa3cd4.
The cleanup was in the pipeline as a minor point ever since we started
eliminating "global" consts in the late 1990-ies. It came up again just
recently, because the semantic completion started to offer odd things like
"dummy_pattern" to the unaware user (items are sorted according to
qualified name length, similar to find_theorems).
I've also made a systematic check of "all" as free variable vs. former
constant, and the above changeset should be clean in this respect. There
are about 5 situations in Isabelle + AFP where regular theories introduce
their own "all" constants, but this is perfectly OK and now without any
name space conflict.
Makarius
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
