doc-src/IsarImplementation/Thy/ROOT.ML

Added [simp]-lemmas "in_inv_image" and "in_lex_prod" in the spirit of "in_measure".
This simplifies some proofs.

(* $Id$ *)

use_thy "prelim";
use_thy "logic";
use_thy "tactic";
use_thy "proof";
use_thy "locale";
use_thy "integration";
use_thy "ML";