/[mojave]/metaprl/theories/tactic/top_conversionals.ml
ViewVC logotype

Diff of /metaprl/theories/tactic/top_conversionals.ml

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

revision 3590 by nogin, Thu Apr 25 15:28:40 2002 UTC revision 3591 by nogin, Sun Apr 28 19:51:58 2002 UTC
# Line 376  Line 376 
376   * @item{pair; $(@bf{match}@space (a, b)@space @bf{with}@space u, v @rightarrow c[u, v]) @longleftrightarrow c[a, b]$}   * @item{pair; $(@bf{match}@space (a, b)@space @bf{with}@space u, v @rightarrow c[u, v]) @longleftrightarrow c[a, b]$}
377   * @item{union; $(@bf{match}@space @i{inl}(a)@space @bf{with}@space   * @item{union; $(@bf{match}@space @i{inl}(a)@space @bf{with}@space
378   *                @i{inl}(u) @rightarrow b[u]   *                @i{inl}(u) @rightarrow b[u]
379   *                @mathrel{|} @i{inr}(v) @rightarrow c[v]) @longleftrightarrow b[a]$}   *                | @i{inr}(v) @rightarrow c[v]) @longleftrightarrow b[a]$}
380   * @end[description]   * @end[description]
381   *   *
382   * Each of the modules for functions (Section @reftheory[Itt_rfun]),   * Each of the modules for functions (Section @reftheory[Itt_rfun]),
# Line 388  Line 388 
388   * @tt{Itt_union} adds the @tt{reduceDecideInl} rewrite with   * @tt{Itt_union} adds the @tt{reduceDecideInl} rewrite with
389   * redex $(@bf{match}@space @i{inl}(a)@space @bf{with}@space   * redex $(@bf{match}@space @i{inl}(a)@space @bf{with}@space
390   *                @i{inl}(u) @rightarrow b[u]   *                @i{inl}(u) @rightarrow b[u]
391   *                @mathrel{|} @i{inr}(v) @rightarrow c[v])$   *                | @i{inr}(v) @rightarrow c[v])$
392   *   *
393   * In modules that @tt{include} these three theories, the @tt{reduceC}   * In modules that @tt{include} these three theories, the @tt{reduceC}
394   * conversion will recursively search for applications of these three   * conversion will recursively search for applications of these three

Legend:
Removed from v.3590  
changed lines
  Added in v.3591

  ViewVC Help
Powered by ViewVC 1.1.26