equal
deleted
inserted
replaced
215 qed "rank_mono"; |
215 qed "rank_mono"; |
216 |
216 |
217 Goal "rank(Pow(a)) = succ(rank(a))"; |
217 Goal "rank(Pow(a)) = succ(rank(a))"; |
218 by (rtac (rank RS trans) 1); |
218 by (rtac (rank RS trans) 1); |
219 by (rtac le_anti_sym 1); |
219 by (rtac le_anti_sym 1); |
220 br UN_upper_le 2; |
220 by (rtac UN_upper_le 2); |
221 br UN_least_le 1; |
221 by (rtac UN_least_le 1); |
222 by (auto_tac (claset() addIs [rank_mono], simpset())); |
222 by (auto_tac (claset() addIs [rank_mono], simpset())); |
223 qed "rank_Pow"; |
223 qed "rank_Pow"; |
224 |
224 |
225 Goal "rank(0) = 0"; |
225 Goal "rank(0) = 0"; |
226 by (rtac (rank RS trans) 1); |
226 by (rtac (rank RS trans) 1); |