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

Log of /metaprl/theories/czf/czf_itt_group_bvd.mli

Parent Directory Parent Directory | Revision Log Revision Log


Links to HEAD: (view) (download) (annotate)
Sticky Revision:

Revision 3569 - (view) (download) (annotate) - [select for diffs]
Added Tue Apr 9 05:58:44 2002 UTC (19 years, 2 months ago) by xiny
File length: 1148 byte(s)
Defined "group builder" group_bvd{'h; 'g; 's} which build a group
h from group g where the underlying set of h is s, the operation
and equivalence relation in h are the same as in g. The only use
for the introduction of group_bvd is to make codes cleaner, nicer,
or easier to understand. (See examples in Czf_itt_subgroup,
Czf_itt_cyclic_subgroup, and Czf_itt_hom.)


This form allows you to request diffs between any two revisions of this file. For each of the two "sides" of the diff, enter a numeric revision.

  Diffs between and
  Type of Diff should be a

  ViewVC Help
Powered by ViewVC 1.1.26