equal
deleted
inserted
replaced
80 (Free ("P",varsT --> boolT) $ mk_bodyC vars)); |
80 (Free ("P",varsT --> boolT) $ mk_bodyC vars)); |
81 val small_Collect = mk_CollectC (Abs("x",varsT, |
81 val small_Collect = mk_CollectC (Abs("x",varsT, |
82 Free ("P",varsT --> boolT) $ Bound 0)); |
82 Free ("P",varsT --> boolT) $ Bound 0)); |
83 val impl = implies $ (Mset_incl big_Collect) $ |
83 val impl = implies $ (Mset_incl big_Collect) $ |
84 (Mset_incl small_Collect); |
84 (Mset_incl small_Collect); |
85 in Tactic.prove (Thm.sign_of_thm thm) ["Mset", "P"] [] impl (K (CLASET' blast_tac 1)) end; |
85 in Goal.prove (Thm.sign_of_thm thm) ["Mset", "P"] [] impl (K (CLASET' blast_tac 1)) end; |
86 |
86 |
87 end; |
87 end; |
88 |
88 |
89 |
89 |
90 (*****************************************************************************) |
90 (*****************************************************************************) |