equal
deleted
inserted
replaced
114 fun set_mp_tac i = etac subsetCE i THEN mp_tac i; |
114 fun set_mp_tac i = etac subsetCE i THEN mp_tac i; |
115 |
115 |
116 qed_goal "subset_refl" Set.thy "A <= A" |
116 qed_goal "subset_refl" Set.thy "A <= A" |
117 (fn _=> [ (REPEAT (ares_tac [subsetI] 1)) ]); |
117 (fn _=> [ (REPEAT (ares_tac [subsetI] 1)) ]); |
118 |
118 |
119 Goal "!!A B C. [| A<=B; B<=C |] ==> A<=C"; |
119 Goal "[| A<=B; B<=C |] ==> A<=C"; |
120 by (rtac subsetI 1); |
120 by (rtac subsetI 1); |
121 by (REPEAT (eresolve_tac [asm_rl, subsetD] 1)); |
121 by (REPEAT (eresolve_tac [asm_rl, subsetD] 1)); |
122 qed "subset_trans"; |
122 qed "subset_trans"; |
123 |
123 |
124 |
124 |