equal
deleted
inserted
replaced
171 case (Thm.concl_of st, Thm.prop_of th) of |
171 case (Thm.concl_of st, Thm.prop_of th) of |
172 (@{const Trueprop} $ (Var _ $ (c as Free _)), @{const Trueprop} $ _) => |
172 (@{const Trueprop} $ (Var _ $ (c as Free _)), @{const Trueprop} $ _) => |
173 let |
173 let |
174 val cc = Thm.cterm_of ctxt c |
174 val cc = Thm.cterm_of ctxt c |
175 val ct = Thm.dest_arg (Thm.cprop_of th) |
175 val ct = Thm.dest_arg (Thm.cprop_of th) |
176 in resolve_tac ctxt [th] i (Drule.instantiate' [] [SOME (Thm.lambda cc ct)] st) end |
176 in resolve_tac ctxt [th] i (Thm.instantiate' [] [SOME (Thm.lambda cc ct)] st) end |
177 | _ => resolve_tac ctxt [th] i st |
177 | _ => resolve_tac ctxt [th] i st |
178 |
178 |
179 (*Permits forward proof from rules that discharge assumptions. The supplied proof state st, |
179 (*Permits forward proof from rules that discharge assumptions. The supplied proof state st, |
180 e.g. from conj_forward, should have the form |
180 e.g. from conj_forward, should have the form |
181 "[| P' ==> ?P; Q' ==> ?Q |] ==> ?P & ?Q" |
181 "[| P' ==> ?P; Q' ==> ?Q |] ==> ?P & ?Q" |