[isabelle-dev] Legacy feature

[Christian Sternagel]

Dear Developers,

I find it slightly odd to get warnings like

### Legacy feature! Old 'axioms' command -- use 'axiomatization' instead

in places like HOL.thy. The reason is that (at least for me) this theory 
is the first place to look how things are done, but the warning (which I 
only see when actually loading the theory -- and usually I only browse 
the corresponding html page) indicates that things should be done 
differently.

Why not use 'axiomatization' here?

cheers

chris