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

author | lcp |

Fri, 21 Oct 1994 09:58:05 +0100 | |

changeset 652 | ff4d4d7fcb7f |

parent 651 | 4b0455fbcc49 |

child 653 | 6eeff82979df |

ZF/intr_elim/elim_rls: now includes Pair_inject, since coinductive
definitions may involve ordinary pairs. (HOL/intr_elim does not require
this change)

--- a/src/ZF/intr_elim.ML Fri Oct 21 09:53:38 1994 +0100 +++ b/src/ZF/intr_elim.ML Fri Oct 21 09:58:05 1994 +0100 @@ -119,9 +119,12 @@ (*Includes rules for succ and Pair since they are common constructions*) val elim_rls = [asm_rl, FalseE, succ_neq_0, sym RS succ_neq_0, - Pair_neq_0, sym RS Pair_neq_0, make_elim succ_inject, + Pair_neq_0, sym RS Pair_neq_0, Pair_inject, + make_elim succ_inject, refl_thin, conjE, exE, disjE]; +(*Standard sum/products for datatypes, variant ones for codatatypes; + We always include Pair_inject above*) val sumprod_free_SEs = map (gen_make_elim [conjE,FalseE]) ([Su.distinct, Su.distinct', Su.inl_iff, Su.inr_iff, Pr.pair_iff]