doc-src/IsarAdvanced/Codegen/Thy/ROOT.ML

Modified eqvt_tac to avoid failure due to introduction rules
whose premises contain variables that do not occur in the
conclusion.

(* $Id$ *)

use_thy "Codegen";