equal
deleted
inserted
replaced
50 by (rtac (A_subset_univ RS univ_mono) 2); |
50 by (rtac (A_subset_univ RS univ_mono) 2); |
51 by (fast_tac (ZF_cs addSIs [zero_in_univ, Inl_in_univ, Inr_in_univ, |
51 by (fast_tac (ZF_cs addSIs [zero_in_univ, Inl_in_univ, Inr_in_univ, |
52 Pair_in_univ]) 1); |
52 Pair_in_univ]) 1); |
53 val list_univ = result(); |
53 val list_univ = result(); |
54 |
54 |
55 val list_subset_univ = standard |
55 val list_subset_univ = standard ([list_mono, list_univ] MRS subset_trans); |
56 (list_mono RS (list_univ RSN (2,subset_trans))); |
|
57 |
56 |
58 val major::prems = goal List.thy |
57 val major::prems = goal List.thy |
59 "[| l: list(A); \ |
58 "[| l: list(A); \ |
60 \ c: C(Nil); \ |
59 \ c: C(Nil); \ |
61 \ !!x y. [| x: A; y: list(A) |] ==> h(x,y): C(Cons(x,y)) \ |
60 \ !!x y. [| x: A; y: list(A) |] ==> h(x,y): C(Cons(x,y)) \ |