equal
deleted
inserted
replaced
7 by Kenneth Kunen. Chapter 1, section 6. |
7 by Kenneth Kunen. Chapter 1, section 6. |
8 *) |
8 *) |
9 |
9 |
10 header{*Partial and Total Orderings: Basic Definitions and Properties*} |
10 header{*Partial and Total Orderings: Basic Definitions and Properties*} |
11 |
11 |
12 theory Order = WF + Perm: |
12 theory Order imports WF Perm begin |
13 |
13 |
14 constdefs |
14 constdefs |
15 |
15 |
16 part_ord :: "[i,i]=>o" (*Strict partial ordering*) |
16 part_ord :: "[i,i]=>o" (*Strict partial ordering*) |
17 "part_ord(A,r) == irrefl(A,r) & trans[A](r)" |
17 "part_ord(A,r) == irrefl(A,r) & trans[A](r)" |