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