summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | lcp |

Fri, 09 Sep 1994 11:40:40 +0200 | |

changeset 593 | d4c6e2bdde59 |

parent 592 | 9154d8410514 |

child 594 | 33a6bdb62a18 |

ZF/Zorn/next_bounded: deleted this proof, which was already in comments

src/ZF/Zorn.ML | file | annotate | diff | comparison | revisions |

--- a/src/ZF/Zorn.ML Thu Sep 08 13:17:57 1994 +0200 +++ b/src/ZF/Zorn.ML Fri Sep 09 11:40:40 1994 +0200 @@ -36,14 +36,6 @@ by (assume_tac 1); val increasingD2 = result(); -(*???????????????????????????????????????????????????????????????? -goal Zorn.thy - "!!next S. [| X : Pow(S); next: increasing(S) |] ==> next`X : Pow(S)"; -by (eresolve_tac [increasingD1 RS apply_type] 1); -by (assume_tac 1); -val next_bounded = result(); -*) - (*Introduction rules*) val [TFin_nextI, Pow_TFin_UnionI] = TFin.intrs; val TFin_UnionI = PowI RS Pow_TFin_UnionI;