/[mojave]/metaprl/theories/base/base_rewrite.ml
ViewVC logotype

Diff of /metaprl/theories/base/base_rewrite.ml

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

revision 3583 by nogin, Thu Jul 5 21:15:43 2001 UTC revision 3584 by nogin, Thu Apr 25 15:28:40 2002 UTC
# Line 98  Line 98 
98    
99  (*!  (*!
100   * @begin[doc]   * @begin[doc]
101   * The @Comment!rewrite[rewriteAxiom2] conditional rewrite provides a link to the primitive   * The @tt[rewriteAxiom2] conditional rewrite provides a link to the primitive
102   * rewriter: a proof of $<<Perv!"rewrite"{'a; 'b}>>$ shows that the terms   * rewriter: a proof of $<<Perv!"rewrite"{'a; 'b}>>$ shows that the terms
103   * $a$ and $b$ are computationally equivalent.   * $a$ and $b$ are computationally equivalent.
104   * @end[doc]   * @end[doc]

Legend:
Removed from v.3583  
changed lines
  Added in v.3584

  ViewVC Help
Powered by ViewVC 1.1.26