equal
deleted
inserted
replaced
92 |
92 |
93 syntax |
93 syntax |
94 "@SL" :: "['a set, 'a potype] => bool" ("_ <<= _" [51,50]50) |
94 "@SL" :: "['a set, 'a potype] => bool" ("_ <<= _" [51,50]50) |
95 |
95 |
96 translations |
96 translations |
97 "S <<= cl" == "S : sublattice ``` {cl}" |
97 "S <<= cl" == "S : sublattice `` {cl}" |
98 |
98 |
99 constdefs |
99 constdefs |
100 dual :: "'a potype => 'a potype" |
100 dual :: "'a potype => 'a potype" |
101 "dual po == (| pset = po.<A>, order = converse (po.<r>) |)" |
101 "dual po == (| pset = po.<A>, order = converse (po.<r>) |)" |
102 |
102 |
119 locale CLF = CL + |
119 locale CLF = CL + |
120 fixes |
120 fixes |
121 f :: "'a => 'a" |
121 f :: "'a => 'a" |
122 P :: "'a set" |
122 P :: "'a set" |
123 assumes |
123 assumes |
124 f_cl "f : CLF```{cl}" |
124 f_cl "f : CLF``{cl}" |
125 defines |
125 defines |
126 P_def "P == fix f A" |
126 P_def "P == fix f A" |
127 |
127 |
128 |
128 |
129 locale Tarski = CLF + |
129 locale Tarski = CLF + |