equal
deleted
inserted
replaced
152 (atac 1), |
152 (atac 1), |
153 (strip_tac 1), |
153 (strip_tac 1), |
154 (rtac minimal_lift 1) |
154 (rtac minimal_lift 1) |
155 ]); |
155 ]); |
156 |
156 |
157 val thelub_lift1a = lub_lift1a RS thelubI; |
157 bind_thm ("thelub_lift1a", lub_lift1a RS thelubI); |
158 (* |
158 (* |
159 [| is_chain ?Y1; ? i x. ?Y1 i = Iup x |] ==> |
159 [| is_chain ?Y1; ? i x. ?Y1 i = Iup x |] ==> |
160 lub (range ?Y1) = Iup (lub (range (%i. Ilift (LAM x. x) (?Y1 i)))) |
160 lub (range ?Y1) = Iup (lub (range (%i. Ilift (LAM x. x) (?Y1 i)))) |
161 *) |
161 *) |
162 |
162 |
163 val thelub_lift1b = lub_lift1b RS thelubI; |
163 bind_thm ("thelub_lift1b", lub_lift1b RS thelubI); |
164 (* |
164 (* |
165 [| is_chain ?Y1; ! i x. ?Y1 i ~= Iup x |] ==> |
165 [| is_chain ?Y1; ! i x. ?Y1 i ~= Iup x |] ==> |
166 lub (range ?Y1) = UU_lift |
166 lub (range ?Y1) = UU_lift |
167 *) |
167 *) |
168 |
168 |