[isabelle-dev] Legacy feature

Christian Sternagel c-sterna at jaist.ac.jp
Fri Feb 17 03:16:26 CET 2012

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 

Why not use 'axiomatization' here?



More information about the isabelle-dev mailing list