167 Goalw [lesspoll_def] |
167 Goalw [lesspoll_def] |
168 "[| X lesspoll Y; Y lesspoll Z |] ==> X lesspoll Z"; |
168 "[| X lesspoll Y; Y lesspoll Z |] ==> X lesspoll Z"; |
169 by (blast_tac (claset() addSEs [eqpollE] addIs [eqpollI, lepoll_trans]) 1); |
169 by (blast_tac (claset() addSEs [eqpollE] addIs [eqpollI, lepoll_trans]) 1); |
170 qed "lesspoll_trans"; |
170 qed "lesspoll_trans"; |
171 |
171 |
|
172 Goalw [lesspoll_def] |
|
173 "[| X lepoll Y; Y lesspoll Z |] ==> X lesspoll Z"; |
|
174 by (blast_tac (claset() addSEs [eqpollE] addIs [eqpollI, lepoll_trans]) 1); |
|
175 qed "lesspoll_trans1"; |
|
176 |
172 Goalw [lesspoll_def] |
177 Goalw [lesspoll_def] |
173 "[| X lesspoll Y; Y lepoll Z |] ==> X lesspoll Z"; |
178 "[| X lesspoll Y; Y lepoll Z |] ==> X lesspoll Z"; |
174 by (blast_tac (claset() addSEs [eqpollE] addIs [eqpollI, lepoll_trans]) 1); |
179 by (blast_tac (claset() addSEs [eqpollE] addIs [eqpollI, lepoll_trans]) 1); |
175 qed "lesspoll_lepoll_lesspoll"; |
180 qed "lesspoll_trans2"; |
176 |
|
177 Goalw [lesspoll_def] |
|
178 "[| X lesspoll Y; Z lepoll X |] ==> Z lesspoll Y"; |
|
179 by (blast_tac (claset() addSEs [eqpollE] addIs [eqpollI, lepoll_trans]) 1); |
|
180 qed "lepoll_lesspoll_lesspoll"; |
|
181 |
181 |
182 |
182 |
183 (** LEAST -- the least number operator [from HOL/Univ.ML] **) |
183 (** LEAST -- the least number operator [from HOL/Univ.ML] **) |
184 |
184 |
185 val [premP,premOrd,premNot] = Goalw [Least_def] |
185 val [premP,premOrd,premNot] = Goalw [Least_def] |