Changes between Version 3 and Version 4 of TypeFunctionsSynTC


Ignore:
Timestamp:
Dec 5, 2006 7:49:00 AM (9 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