src/ZF/InfDatatype.ML
changeset 9211 6236c5285bd8
parent 9174 6ef054f33f83
child 9907 473a6604da94
     1.1 --- a/src/ZF/InfDatatype.ML	Fri Jun 30 12:49:11 2000 +0200
     1.2 +++ b/src/ZF/InfDatatype.ML	Fri Jun 30 12:51:30 2000 +0200
     1.3 @@ -71,9 +71,9 @@
     1.4  qed "Card_fun_in_Vcsucc";
     1.5  
     1.6  (*Proved explicitly, in theory InfDatatype, to allow the bind_thm calls below*)
     1.7 -qed_goal "Limit_csucc" InfDatatype.thy
     1.8 -    "!!K. InfCard(K) ==> Limit(csucc(K))"
     1.9 -  (fn _ => [etac (InfCard_csucc RS InfCard_is_Limit) 1]);
    1.10 +Goal "InfCard(K) ==> Limit(csucc(K))";
    1.11 +by (etac (InfCard_csucc RS InfCard_is_Limit) 1);
    1.12 +qed "Limit_csucc";
    1.13  
    1.14  bind_thm ("Pair_in_Vcsucc",  Limit_csucc RSN (3, Pair_in_VLimit));
    1.15  bind_thm ("Inl_in_Vcsucc",   Limit_csucc RSN (2, Inl_in_VLimit));