src/HOL/IMPP/ROOT.ML
2009-11-11 wenzelm 2009-11-11 uniform use of simultabeous use_thys;
2000-05-30 wenzelm 2000-05-30 cleaned up;
2000-01-31 oheimb 2000-01-31 added IMPP to HOL