equal
deleted
inserted
replaced
223 "[| p:A; !!z. z:A ==> p=z --> R |] ==> R"; |
223 "[| p:A; !!z. z:A ==> p=z --> R |] ==> R"; |
224 by (rtac mp 1); |
224 by (rtac mp 1); |
225 by (REPEAT (resolve_tac (refl::prems) 1)); |
225 by (REPEAT (resolve_tac (refl::prems) 1)); |
226 qed "setup_induction"; |
226 qed "setup_induction"; |
227 |
227 |
|
228 Goal "A = B ==> (x : A) = (x : B)"; |
|
229 by (Asm_simp_tac 1); |
|
230 qed "eqset_imp_iff"; |
|
231 |
228 |
232 |
229 section "The universal set -- UNIV"; |
233 section "The universal set -- UNIV"; |
230 |
234 |
231 Goalw [UNIV_def] "x : UNIV"; |
235 Goalw [UNIV_def] "x : UNIV"; |
232 by (rtac CollectI 1); |
236 by (rtac CollectI 1); |