| changeset 12338 | de0f4a63baa5 |
| parent 12114 | a8e860c86252 |
| child 14981 | e73f8140af78 |
| 12337:7c6a970f0808 | 12338:de0f4a63baa5 |
|---|---|
7 *) |
7 *) |
8 |
8 |
9 Porder0 = Main + |
9 Porder0 = Main + |
10 |
10 |
11 (* introduce a (syntactic) class for the constant << *) |
11 (* introduce a (syntactic) class for the constant << *) |
12 axclass sq_ord<term |
12 axclass sq_ord < type |
13 |
13 |
14 (* characteristic constant << for po *) |
14 (* characteristic constant << for po *) |
15 consts |
15 consts |
16 "<<" :: "['a,'a::sq_ord] => bool" (infixl 55) |
16 "<<" :: "['a,'a::sq_ord] => bool" (infixl 55) |
17 |
17 |