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

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

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

revision 3554 by xiny, Sun Mar 24 07:43:47 2002 UTC revision 3555 by xiny, Tue Apr 2 07:49:49 2002 UTC
# Line 25  Line 25 
25  open Base_dtactic  open Base_dtactic
26  open Base_auto_tactic  open Base_auto_tactic
27    
28  declare abel{'g; 'r}  declare abel{'g}
29    
30  rewrite unfold_abel: abel{'g; 'r} <-->  rewrite unfold_abel: abel{'g} <-->
31     (group{'g} & isset{'r} & equiv{car{'g}; 'r} & (all a: set. all b: set. (mem{'a; car{'g}} => mem{'b; car{'g}} => equiv{car{'g}; 'r; op{'g; 'a; 'b}; op{'g; 'b; 'a}})))     (group{'g} & (all a: set. all b: set. (mem{'a; car{'g}} => mem{'b; car{'g}} => equiv{car{'g}; eqG{'g}; op{'g; 'a; 'b}; op{'g; 'b; 'a}})))

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

  ViewVC Help
Powered by ViewVC 1.1.26