[isabelle-dev] NEWS: constants of Pure use more conventional names

[Makarius]

* 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