/[mojave]/metaprl/theories/czf/czf_itt_group.mli
ViewVC logotype

Diff of /metaprl/theories/czf/czf_itt_group.mli

Parent Directory Parent Directory | Revision Log Revision Log | View Patch Patch

revision 3552 by xiny, Mon Mar 4 02:20:01 2002 UTC revision 3553 by xiny, Tue Apr 2 07:45:26 2002 UTC
# Line 1  Line 1 
1  include Itt_record_label0  include Itt_record_label0
 include Czf_itt_set  
2  include Czf_itt_member  include Czf_itt_member
3  include Czf_itt_eq  include Czf_itt_eq
4  include Czf_itt_dall  include Czf_itt_dall
5  include Czf_itt_and  include Czf_itt_and
6    include Czf_itt_equiv
7    
8  open Mp_debug  open Mp_debug
9  open Refiner.Refiner.TermType  open Refiner.Refiner.TermType
# Line 28  Line 28 
28  open Base_auto_tactic  open Base_auto_tactic
29    
30  declare group{'g}  declare group{'g}
31  declare car{'g}   (* The "carrier" set for the group *)  declare car{'g}         (* The "carrier" set for the group *)
32    declare eqG{'g}         (* The equivalence relation for the group *)
33    (*declare eqG{'g; 'a; 'b} (* a and b are equivalent in the group *)*)
34  declare op{'g; 'a; 'b}  declare op{'g; 'a; 'b}
35  declare id{'g}  declare id{'g}
36  declare inv{'g; 'a}  declare inv{'g; 'a}
37  (*declare eqElem{'s; 'a; 'b}*)  (*
38    rewrite unfold_eqG : eqG{'g; 'a; 'b} <-->
39  prec prec_op     equiv{car{'g}; eqG{'g}; 'a; 'b}
40    
41    topval fold_eqG : conv
42    *)
43  topval groupCancelLeftT : int -> tactic  topval groupCancelLeftT : int -> tactic
44  topval groupCancelRightT : int -> tactic  topval groupCancelRightT : int -> tactic
45  (*topval groupCancelLeftT : term -> term -> tactic  topval uniqueInvLeftT : int -> tactic
46  topval groupCancelRightT : term -> term -> tactic*)  topval uniqueInvRightT : int -> tactic

Legend:
Removed from v.3552  
changed lines
  Added in v.3553

  ViewVC Help
Powered by ViewVC 1.1.26