equal
deleted
inserted
replaced
236 (** ~ b=a ==> ~ a=b **) |
236 (** ~ b=a ==> ~ a=b **) |
237 val [not_sym] = compose(sym,2,contrapos); |
237 val [not_sym] = compose(sym,2,contrapos); |
238 |
238 |
239 (*Substitution: rule and tactic*) |
239 (*Substitution: rule and tactic*) |
240 bind_thm ("ssubst", sym RS subst); |
240 bind_thm ("ssubst", sym RS subst); |
241 fun stac th = CHANGED o rtac (th RS ssubst); |
241 |
|
242 (*Fails unless the substitution has an effect*) |
|
243 fun stac th = CHANGED_GOAL (rtac (th RS ssubst)); |
242 |
244 |
243 (*A special case of ex1E that would otherwise need quantifier expansion*) |
245 (*A special case of ex1E that would otherwise need quantifier expansion*) |
244 qed_goal "ex1_equalsE" IFOL.thy |
246 qed_goal "ex1_equalsE" IFOL.thy |
245 "[| EX! x. P(x); P(a); P(b) |] ==> a=b" |
247 "[| EX! x. P(x); P(a); P(b) |] ==> a=b" |
246 (fn prems => |
248 (fn prems => |