src/HOL/MicroJava/J/Decl.ML

deactivate Rational_Numbers (tmp!);

(*  Title:      HOL/MicroJava/J/Decl.ML
    ID:         $Id$
    Author:     David von Oheimb
    Copyright   1999 Technische Universitaet Muenchen
*)

Goal "finite {C. is_class G C}";
by (fold_goals_tac [dom_def]);
by (rtac finite_dom_map_of 1);
qed "finite_is_class";