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

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

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

revision 3592 by kopylov, Tue Dec 4 02:49:30 2001 UTC revision 3593 by kopylov, Tue Apr 30 00:41:41 2002 UTC
# Line 265  Line 265 
265  interactive redAInCSpace {|intro[] |} 'H :  interactive redAInCSpace {|intro[] |} 'H :
266     sequent['ext] {'H >- redA IN cspace }     sequent['ext] {'H >- redA IN cspace }
267    
 (*! @docoff *)  
   
268    
269  interactive cspaceElim {|elim[] |} 'H 'J:  interactive cspaceElim {|elim[] |} 'H 'J:
270     sequent['ext]{'H; a:int; b:int; c:int; color:atom; e:record; 'J[rcrd["color":t]{'color;point{'a;'b; 'c; 'e}}] >- 'C[rcrd["color":t]{'color;point{'a;'b; 'c; 'e}}] } -->     sequent['ext]{'H; a:int; b:int; c:int; color:atom; e:record; 'J[rcrd["color":t]{'color;point{'a;'b; 'c; 'e}}] >- 'C[rcrd["color":t]{'color;point{'a;'b; 'c; 'e}}] } -->

Legend:
Removed from v.3592  
changed lines
  Added in v.3593

  ViewVC Help
Powered by ViewVC 1.1.26