/[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 3555 by xiny, Mon Mar 11 09:58:58 2002 UTC revision 3556 by xiny, Tue Apr 2 08:08:36 2002 UTC
# Line 19  Line 19 
19  open Base_dtactic  open Base_dtactic
20  open Base_auto_tactic  open Base_auto_tactic
21    
22  declare subgroup{'g; 's}  declare subgroup{'s; 'g}
23    
24  rewrite unfold_subgroup : subgroup{'g; 's} <-->  rewrite unfold_subgroup : subgroup{'s; 'g} <-->
25     (group{'g} & group{'s} & 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}})))     (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})))
26    
27  topval subgroupIsectT: term -> term -> tactic  topval subgroupIsectT: term -> term -> tactic

Legend:
Removed from v.3555  
changed lines
  Added in v.3556

  ViewVC Help
Powered by ViewVC 1.1.26