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
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
