isabelle: src/HOL/MicroJava/J/Decl.ML@33e290a70445 (annotated)

9348 f495dba0cb07 corrections (cast relation, Prog.ML -> Decl.ML) oheimb parents: diff changeset	1	(* Title: HOL/MicroJava/J/Decl.ML
f495dba0cb07 corrections (cast relation, Prog.ML -> Decl.ML) oheimb parents: diff changeset	2	ID: $Id$
f495dba0cb07 corrections (cast relation, Prog.ML -> Decl.ML) oheimb parents: diff changeset	3	Author: David von Oheimb
f495dba0cb07 corrections (cast relation, Prog.ML -> Decl.ML) oheimb parents: diff changeset	4	Copyright 1999 Technische Universitaet Muenchen
f495dba0cb07 corrections (cast relation, Prog.ML -> Decl.ML) oheimb parents: diff changeset	5	*)
f495dba0cb07 corrections (cast relation, Prog.ML -> Decl.ML) oheimb parents: diff changeset	6
10925 5ffe7ed8899a is_class and class now as defs (rather than translations); corrected Digest.thy oheimb parents: 10613 diff changeset	7	Goalw [is_class_def, class_def] "finite {C. is_class G C}";
10613 78b1d6c3ee9c improved superclass entry for classes and definition status of is_class, class oheimb parents: 10042 diff changeset	8	by (fold_goals_tac [dom_def]);
78b1d6c3ee9c improved superclass entry for classes and definition status of is_class, class oheimb parents: 10042 diff changeset	9	by (rtac finite_dom_map_of 1);
78b1d6c3ee9c improved superclass entry for classes and definition status of is_class, class oheimb parents: 10042 diff changeset	10	qed "finite_is_class";
9348 f495dba0cb07 corrections (cast relation, Prog.ML -> Decl.ML) oheimb parents: diff changeset	11