Seeking description of consistency correctness-condition

Hello,

  I'm looking for a description of the 'consistency' correctness-
  condition and the situations where it is required. Particularly, a
  statement of the template formula one must prove to establish consistency.
  
  After looking through some old papers like 'Muzalewski1993 PCMizar',
  and Matuszewski+Rudnicki 'Mizar: the first 30 years', I either couldn't
  find it, or only a brief mention that it is required for 'definitions
  per cases'.
  
  Searching the MML, consistency is usually demonstrated simply as:
        consistency;    (due to disjointness of if/otherwise ?) 
        
  But in the non-trivial cases, the condition being proved isn't
  obvious to me.

  Thanks,

-Greg Frascadore

-- 
View this message in context: http://www.nabble.com/Seeking-description-of-consistency-correctness-condition-tp26027415p26027415.html
Sent from the Mizar mailing list archive at Nabble.com.