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

author | paulson |

Fri, 16 Jun 2000 13:15:40 +0200 | |

changeset 9075 | e8521ed7f35b |

parent 9074 | 2313ddc415a1 |

child 9076 | 108ec332625d |

Finally "AddEs [equalityE]" is IN and "AddDs [equals0D, sym RS equals0D]" is OUT

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

--- a/src/HOL/Set.ML Fri Jun 16 13:15:04 2000 +0200 +++ b/src/HOL/Set.ML Fri Jun 16 13:15:40 2000 +0200 @@ -212,10 +212,7 @@ by (REPEAT (resolve_tac (prems RL [equalityD1,equalityD2]) 1)); qed "equalityE"; -(*This could be tried. Most things build fine with it. However, some proofs - become very slow or even fail. - AddEs [equalityE]; -*) +AddEs [equalityE]; val major::prems = Goal "[| A = B; [| c:A; c:B |] ==> P; [| c~:A; c~:B |] ==> P |] ==> P"; @@ -295,9 +292,6 @@ by (Blast_tac 1) ; qed "equals0D"; -(* [| A = {}; a : A |] ==> R *) -AddDs [equals0D, sym RS equals0D]; - Goalw [Ball_def] "Ball {} P = True"; by (Simp_tac 1); qed "ball_empty";