src/HOL/IMPP/ROOT.ML

Implement previous fix (don't duplicate ext_def) correctly.

(*  Title:      HOL/IMPP/ROOT.ML
    ID:         $Id$
    Author:     David von Oheimb
    Copyright   1999 TUM
*)

time_use_thy "EvenOdd";