Changes between Version 3 and Version 4 of TypeFunctionsSynTC


Ignore:
Timestamp:
Dec 5, 2006 7:49:00 AM (7 years ago)
Author:
simonpj
Comment:

--

Legend:

Unmodified
Added
Removed
Modified
  • TypeFunctionsSynTC

    v3 v4  
    153153The trouble here is that 
    154154 
    155 * the axiom system Ax is confluent but if we included the local assumptions C 
    156  
    157 * the combined system Ax /\ C is non-confluent (interpreted as a rewrite system) 
     155 * the axiom system Ax is confluent, but 
     156 * if we include the local assumptions C, the combined system Ax /\ C is non-confluent (interpreted as a rewrite system) 
    158157 
    159158