equal
deleted
inserted
replaced
68 by (rtac (major RS exE) 1); |
68 by (rtac (major RS exE) 1); |
69 by (REPEAT (eresolve_tac (prems @ [asm_rl,conjE]) 1)); |
69 by (REPEAT (eresolve_tac (prems @ [asm_rl,conjE]) 1)); |
70 qed "bexE"; |
70 qed "bexE"; |
71 |
71 |
72 (*Trival rewrite rule; (! x:A.P)=P holds only if A is nonempty!*) |
72 (*Trival rewrite rule; (! x:A.P)=P holds only if A is nonempty!*) |
73 val prems = goal Set.thy |
73 goal Set.thy "(! x:A. True) = True"; |
74 "(! x:A. True) = True"; |
|
75 by (REPEAT (ares_tac [TrueI,ballI,iffI] 1)); |
74 by (REPEAT (ares_tac [TrueI,ballI,iffI] 1)); |
76 qed "ball_rew"; |
75 qed "ball_rew"; |
|
76 Addsimps [ball_rew]; |
77 |
77 |
78 (** Congruence rules **) |
78 (** Congruence rules **) |
79 |
79 |
80 val prems = goal Set.thy |
80 val prems = goal Set.thy |
81 "[| A=B; !!x. x:B ==> P(x) = Q(x) |] ==> \ |
81 "[| A=B; !!x. x:B ==> P(x) = Q(x) |] ==> \ |