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

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

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

revision 3583 by nogin, Thu Mar 7 22:55:35 2002 UTC revision 3584 by nogin, Thu Apr 25 15:28:40 2002 UTC
# Line 494  Line 494 
494   * The following rule establishes that @tt[assert] is always decidable.   * The following rule establishes that @tt[assert] is always decidable.
495   * @end[doc]   * @end[doc]
496   *)   *)
497  interactive assert_decidable {| intro [] |} 'H:  interactive assert_is_decidable {| intro [] |} 'H:
498     [wf] sequent [squash] { 'H >- 't IN bool } -->     [wf] sequent [squash] { 'H >- 't IN bool } -->
499     sequent ['ext] { 'H >- decidable{."assert"{'t}} }     sequent ['ext] { 'H >- decidable{."assert"{'t}} }
500    

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

  ViewVC Help
Powered by ViewVC 1.1.26