changeset 3888 | 85eb8e24c5ff |
parent 2469 | b50b8c0eec01 |
child 4091 | 771b1f6422a8 |
--- a/src/ZF/InfDatatype.ML Thu Oct 16 13:38:28 1997 +0200 +++ b/src/ZF/InfDatatype.ML Thu Oct 16 13:38:47 1997 +0200 @@ -7,7 +7,8 @@ *) val fun_Limit_VfromE = - [apply_funtype, InfCard_csucc RS InfCard_is_Limit] MRS Limit_VfromE + [apply_funtype, InfCard_csucc RS InfCard_is_Limit] MRS + transfer InfDatatype.thy Limit_VfromE |> standard; goal InfDatatype.thy