NEWS
changeset 56245 84fc7dfa3cd4
parent 56232 31e283f606e2
child 56248 67dc9549fa15
     1.1 --- a/NEWS	Fri Mar 21 15:12:03 2014 +0100
     1.2 +++ b/NEWS	Fri Mar 21 20:33:56 2014 +0100
     1.3 @@ -71,6 +71,34 @@
     1.4  
     1.5  *** Pure ***
     1.6  
     1.7 +* Basic constants of Pure use more conventional names and are always
     1.8 +qualified.  Rare INCOMPATIBILITY, but with potentially serious
     1.9 +consequences, notably for tools in Isabelle/ML.  The following
    1.10 +renaming needs to be applied:
    1.11 +
    1.12 +  ==             ~>  Pure.eq
    1.13 +  ==>            ~>  Pure.imp
    1.14 +  all            ~>  Pure.all
    1.15 +  TYPE           ~>  Pure.type
    1.16 +  dummy_pattern  ~>  Pure.dummy_pattern
    1.17 +
    1.18 +Systematic porting works by using the following theory setup on a
    1.19 +*previous* Isabelle version to introduce the new name accesses for the
    1.20 +old constants:
    1.21 +
    1.22 +setup {*
    1.23 +  fn thy => thy
    1.24 +    |> Sign.root_path
    1.25 +    |> Sign.const_alias (Binding.qualify true "Pure" @{binding eq}) "=="
    1.26 +    |> Sign.const_alias (Binding.qualify true "Pure" @{binding imp}) "==>"
    1.27 +    |> Sign.const_alias (Binding.qualify true "Pure" @{binding all}) "all"
    1.28 +    |> Sign.restore_naming thy
    1.29 +*}
    1.30 +
    1.31 +Thus ML antiquotations like @{const_name Pure.eq} may be used already.
    1.32 +Later the application is moved to the current Isabelle version, and
    1.33 +the auxiliary aliases are deleted.
    1.34 +
    1.35  * Low-level type-class commands 'classes', 'classrel', 'arities' have
    1.36  been discontinued to avoid the danger of non-trivial axiomatization
    1.37  that is not immediately visible.  INCOMPATIBILITY, use regular