changeset 15531 | 08c8dad8e399 |
parent 11260 | b736de4cb913 |
child 15661 | 9ef583b08647 |
--- a/src/Cube/ex/ex.ML Fri Feb 11 18:51:00 2005 +0100 +++ b/src/Cube/ex/ex.ML Sun Feb 13 17:15:14 2005 +0100 @@ -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";