| changeset 41526 | 54b4686704af |
| parent 41229 | d797baa3d57c |
| child 42284 | 326f57825e1a |
--- a/src/Cube/Cube.thy Wed Jan 12 15:53:37 2011 +0100 +++ b/src/Cube/Cube.thy Wed Jan 12 16:33:04 2011 +0100 @@ -76,11 +76,11 @@ lemma imp_elim: assumes "f:A->B" and "a:A" and "f^a:B ==> PROP P" - shows "PROP P" by (rule app prems)+ + shows "PROP P" by (rule app assms)+ lemma pi_elim: assumes "F:Prod(A,B)" and "a:A" and "F^a:B(a) ==> PROP P" - shows "PROP P" by (rule app prems)+ + shows "PROP P" by (rule app assms)+ locale L2 =