| changeset 694 | c7d592f6312a |
| parent 438 | 52e8393ccd77 |
| child 760 | f0200e91b272 |
--- a/src/ZF/ex/Ramsey.ML Thu Nov 03 13:42:39 1994 +0100 +++ b/src/ZF/ex/Ramsey.ML Thu Nov 03 16:05:22 1994 +0100 @@ -42,8 +42,8 @@ (*** Atleast ***) -goalw Ramsey.thy [Atleast_def,inj_def] "Atleast(0,A)"; -by (fast_tac (ZF_cs addIs [PiI]) 1); +goalw Ramsey.thy [Atleast_def, inj_def, Pi_def, function_def] "Atleast(0,A)"; +by (fast_tac ZF_cs 1); val Atleast0 = result(); val [major] = goalw Ramsey.thy [Atleast_def]