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

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

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

revision 3557 by xiny, Mon Mar 11 10:04:22 2002 UTC revision 3558 by xiny, Tue Apr 2 08:27:06 2002 UTC
# Line 1  Line 1 
1  include Czf_itt_group  include Czf_itt_group
2  include Czf_itt_cyclic_subgroup  include Czf_itt_cyclic_subgroup
 include Czf_itt_subgroup  
 include Czf_itt_subset  
 include Itt_logic  
3    
4  open Printf  open Printf
5  open Mp_debug  open Mp_debug
# Line 30  Line 27 
27  declare cycgroup{'g; 'a}  declare cycgroup{'g; 'a}
28    
29  rewrite unfold_cycgroup : cycgroup{'g; 'a} <-->  rewrite unfold_cycgroup : cycgroup{'g; 'a} <-->
30     cyc_subg{'g; 'g; 'a}     (group{'g} & mem{'a; car{'g}} & equal{car{'g}; collect{int; x. power{'g; 'a; 'x}}})
31    
32  topval fold_cycgroup : conv  topval fold_cycgroup : conv
33  topval cycgroupAbelT: term -> tactic  topval cycgroupAbelT: term -> tactic

Legend:
Removed from v.3557  
changed lines
  Added in v.3558

  ViewVC Help
Powered by ViewVC 1.1.26