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

author | paulson |

Thu, 29 Jun 2000 12:14:45 +0200 | |

changeset 9186 | 7b2f4e6538b4 |

parent 9185 | 30d46270a427 |

child 9187 | 68ecc04785f1 |

now uses equalityCE, which usually is more efficent than equalityE

src/HOL/Set.ML | file | annotate | diff | comparison | revisions |

--- a/src/HOL/Set.ML Thu Jun 29 12:14:04 2000 +0200 +++ b/src/HOL/Set.ML Thu Jun 29 12:14:45 2000 +0200 @@ -210,14 +210,14 @@ by (REPEAT (resolve_tac (prems RL [equalityD1,equalityD2]) 1)); qed "equalityE"; -AddEs [equalityE]; - val major::prems = Goal "[| A = B; [| c:A; c:B |] ==> P; [| c~:A; c~:B |] ==> P |] ==> P"; by (rtac (major RS equalityE) 1); by (REPEAT (contr_tac 1 ORELSE eresolve_tac ([asm_rl,subsetCE]@prems) 1)); qed "equalityCE"; +AddEs [equalityCE]; + (*Lemma for creating induction formulae -- for "pattern matching" on p To make the induction hypotheses usable, apply "spec" or "bspec" to put universal quantifiers over the free variables in p. *)