| changeset 15661 | 9ef583b08647 |
| parent 15531 | 08c8dad8e399 |
--- a/src/Cube/ex/ex.ML Thu Apr 07 09:24:35 2005 +0200 +++ b/src/Cube/ex/ex.ML Thu Apr 07 09:25:33 2005 +0200 @@ -201,7 +201,7 @@ by (EVERY[etac pi_elim 1, assume_tac 1, assume_tac 1]); uresult(); -(* SOME random examples *) +(* Some random examples *) goal LP2.thy "A:* c:A f:A->A |- \ \ Lam a:A. Pi P:A->*.P^c -> (Pi x:A. P^x->P^(f^x)) -> P^a : ?T";