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

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

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

revision 3558 by xiny, Sun Mar 24 08:26:30 2002 UTC revision 3559 by xiny, Tue Apr 2 08:46:33 2002 UTC
# Line 24  Line 24 
24  open Base_dtactic  open Base_dtactic
25  open Base_auto_tactic  open Base_auto_tactic
26    
27  declare hom{'g1; 'g2; 'r1; 'r2; x. 'f['x]}  declare hom{'g1; 'g2; x. 'f['x]}
28    
29  rewrite unfold_hom : hom{'g1; 'g2; 'r1; 'r2; x. 'f['x]} <-->  rewrite unfold_hom : hom{'g1; 'g2; x. 'f['x]} <-->
30     (group{'g1} & group{'g2} & isset{'r1} & isset{'r2} & equiv{car{'g1}; 'r1} & equiv{car{'g2}; 'r2} & fun_set{x. 'f['x]} & "dall"{car{'g1}; a. mem{'f['a]; car{'g2}}} & (all a: set. all b: set. (mem{'a; car{'g1}} => mem{'b; car{'g1}} => equiv{car{'g2}; 'r2; 'f[op{'g1; 'a; 'b}]; op{'g2; 'f['a]; 'f['b]}})))     (group{'g1} & group{'g2} & (all a: set. (mem{'a; car{'g1}} => mem{'f['a]; car{'g2}})) & (all a: set. all b: set. (mem{'a; car{'g1}} => mem{'b; car{'g1}} => equiv{car{'g1}; eqG{'g1}; 'a; 'b} => equiv{car{'g2}; eqG{'g2}; 'f['a]; 'f['b]})) & (all a: set. all b: set. (mem{'a; car{'g1}} => mem{'b; car{'g1}} => equiv{car{'g2}; eqG{'g2}; 'f[op{'g1; 'a; 'b}]; op{'g2; 'f['a]; 'f['b]}})))
31    
32    topval homIdT : int -> tactic
33    topval homInvT : term -> int -> tactic

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

  ViewVC Help
Powered by ViewVC 1.1.26