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

author | paulson |

Thu, 10 Sep 1998 17:20:49 +0200 | |

changeset 5450 | fe9d103464a4 |

parent 5449 | d853d1ac85a3 |

child 5451 | 08ca6e067ee6 |

Changed equals0E back to equals0D and gave it the correct destruct form

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

--- a/src/HOL/Set.ML Thu Sep 10 17:17:22 1998 +0200 +++ b/src/HOL/Set.ML Thu Sep 10 17:20:49 1998 +0200 @@ -115,8 +115,6 @@ by (REPEAT (ares_tac (prems @ [ballI]) 1)); qed "subsetI"; -Blast.overloaded ("op <=", domain_type); (*The <= relation is overloaded*) - (*While (:) is not, its type must be kept for overloading of = to work.*) Blast.overloaded ("op :", domain_type); @@ -257,10 +255,10 @@ [ (blast_tac (claset() addIs [prem RS FalseE]) 1) ]); (*Use for reasoning about disjointness: A Int B = {} *) -qed_goal "equals0E" Set.thy "!!a. [| A={}; a:A |] ==> P" +qed_goal "equals0D" Set.thy "!!a. A={} ==> a ~: A" (fn _ => [ (Blast_tac 1) ]); -AddEs [equals0E, sym RS equals0E]; +AddDs [equals0D, sym RS equals0D]; Goalw [Ball_def] "Ball {} P = True"; by (Simp_tac 1);