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

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

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

revision 3583 by nogin, Sun Jun 24 10:25:49 2001 UTC revision 3584 by nogin, Thu Apr 25 15:28:40 2002 UTC
# Line 4  Line 4 
4   *   *
5   * The @tt{Itt_well_founded} module provides a more convenient   * The @tt{Itt_well_founded} module provides a more convenient
6   * description of well-foundness than the @hrefterm[well_founded_prop]   * description of well-foundness than the @hrefterm[well_founded_prop]
7   * term formalized the the @hreftheory[Itt_rfun] module.  The definition   * term formalized in the @hreftheory[Itt_rfun] module.  The definition
8   * of well-foundness requires the derivation of an induction   * of well-foundness requires the derivation of an induction
9   * principle.   * principle.
10   * @end[doc]   * @end[doc]

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

  ViewVC Help
Powered by ViewVC 1.1.26