1(* ========================================================================= *) 2(* GROUP THEORY TOOLS *) 3(* ========================================================================= *) 4 5signature groupTools = 6sig 7 8(* ------------------------------------------------------------------------- *) 9(* Syntax operations. *) 10(* ------------------------------------------------------------------------- *) 11 12val group_inv_tm : Term.term 13val dest_group_inv : Term.term -> Term.term * Term.term 14val is_group_inv : Term.term -> bool 15 16val group_mult_tm : Term.term 17val dest_group_mult : Term.term -> Term.term * Term.term * Term.term 18val is_group_mult : Term.term -> bool 19 20val group_exp_tm : Term.term 21val dest_group_exp : Term.term -> Term.term * Term.term * Term.term 22val is_group_exp : Term.term -> bool 23 24(* ------------------------------------------------------------------------- *) 25(* AC normalization. *) 26(* ------------------------------------------------------------------------- *) 27 28val group_ac_conv : subtypeTools.named_conv 29 30(* ------------------------------------------------------------------------- *) 31(* Subtype context. *) 32(* ------------------------------------------------------------------------- *) 33 34val group_context : subtypeTools.context2 35 36end 37