1signature finite_groupContext = 2sig 3 4 type subtype_context_element = subtypeTools.subtype_context_element 5 type precontext = subtypeTools.precontext 6 type context = subtypeTools.context 7 8 (* Subtype checking *) 9 10 (* Contextual rewriting *) 11 val finite_group_pc : precontext; 12 val finite_group_c : context; 13 14end 15 16