doc-src/Tutorial/Misc/arith2.ML

* HOL/Library: a collection of generic theories to be used together
with main HOL; the theory loader path already includes this directory
by default; the following existing theories have been moved here:
HOL/Induct/Multiset, HOL/Induct/Acc (as Accessible_Part), HOL/While
(as While_Combinator);

Goal "min i (max j (k*k)) = max (min (k*k) i) (min i (j::nat))";