| changeset 824 | 120fc7e857ba |
| parent 760 | f0200e91b272 |
| child 857 | f5314a7c93f2 |
--- a/src/ZF/func.ML Fri Dec 23 16:26:34 1994 +0100 +++ b/src/ZF/func.ML Fri Dec 23 16:27:07 1994 +0100 @@ -57,7 +57,7 @@ qed "Pi_empty2"; (*The empty function*) -goalw ZF.thy [Pi_def, function_def] "0: 0->A"; +goalw ZF.thy [Pi_def, function_def] "0: Pi(0,B)"; by (fast_tac ZF_cs 1); qed "empty_fun";