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

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

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

revision 3590 by kopylov, Tue Jul 3 23:55:20 2001 UTC revision 3591 by nogin, Sun Apr 28 19:51:58 2002 UTC
# Line 166  Line 166 
166   * in the conclusion and replace them with $x$.   * in the conclusion and replace them with $x$.
167   *   *
168   * This tactic is usually used when we have an assumption $s @in S$,   * This tactic is usually used when we have an assumption $s @in S$,
169   * and want to use the elimination rule corresponding to S.   * and want to use the elimination rule corresponding to $S$.
170   *   *
171   * @end[doc]   * @end[doc]
172   *)   *)
173    
   
 (*! docoff *)  
174  (*  (*
175  interactive cutEqWeak 'H ('s_1='s_2 in 'S) bind{x.'t['x]} 'v 'u :  interactive cutEqWeak 'H ('s_1='s_2 in 'S) bind{x.'t['x]} 'v 'u :
176     [assertion] sequent[squash]{ 'H >- 's_1='s_2 in 'S } -->     [assertion] sequent[squash]{ 'H >- 's_1='s_2 in 'S } -->

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

  ViewVC Help
Powered by ViewVC 1.1.26