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