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

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

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

revision 3559 by xiny, Tue Apr 2 08:08:36 2002 UTC revision 3560 by xiny, Wed Apr 3 05:27:01 2002 UTC
# Line 22  Line 22 
22  declare subgroup{'s; 'g}  declare subgroup{'s; 'g}
23    
24  rewrite unfold_subgroup : subgroup{'s; 'g} <-->  rewrite unfold_subgroup : subgroup{'s; 'g} <-->
25     (group{'s} & group{'g} & subset{car{'s}; car{'g}} & (all a: set. all b: set. (mem{'a; car{'s}} => mem{'b; car{'s}} => equal{op{'s; 'a; 'b}; op{'g; 'a; 'b}})) & (all a: set. all b: set. (equiv{car{'s}; eqG{'s}; 'a; 'b} => equiv{car{'g}; eqG{'g}; 'a; 'b})))     (group{'s} & group{'g} & subset{car{'s}; car{'g}} & (all a: set. all b: set. (mem{'a; car{'s}} => mem{'b; car{'s}} => equiv{car{'s}; eqG{'s}; op{'s; 'a; 'b}; op{'g; 'a; 'b}})) & (all a: set. all b: set. (equiv{car{'s}; eqG{'s}; 'a; 'b} => equiv{car{'g}; eqG{'g}; 'a; 'b})) & (all a: set. all b: set. (mem{'a; car{'s}} => mem{'b; car{'s}} => equiv{car{'g}; eqG{'g}; 'a; 'b} => equiv{car{'s}; eqG{'s}; 'a; 'b})))
26    
27  topval subgroupIsectT: term -> term -> tactic  topval subgroupIsectT: term -> term -> tactic

Legend:
Removed from v.3559  
changed lines
  Added in v.3560

  ViewVC Help
Powered by ViewVC 1.1.26