/[mojave]/metaprl/theories/itt/itt_logic.ml
ViewVC logotype

Diff of /metaprl/theories/itt/itt_logic.ml

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

revision 3583 by nogin, Thu Nov 15 23:03:47 2001 UTC revision 3584 by nogin, Thu Apr 25 15:28:40 2002 UTC
# Line 744  Line 744 
744   * @tactics   * @tactics
745   *   *
746   * The @hreftheory[Itt_logic] module defines several tactics for   * The @hreftheory[Itt_logic] module defines several tactics for
747   * reasoning the the @Nuprl type theory.  The tactics perform   * reasoning in the @Nuprl type theory.  The tactics perform
748   * @emph{generic} reasoning of @Nuprl sequents.   * @emph{generic} reasoning of @Nuprl sequents.
749   *   *
750   * @begin[description]   * @begin[description]

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

  ViewVC Help
Powered by ViewVC 1.1.26