summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

src/HOL/Set.thy

changeset 19233 | 77ca20b0ed77 |

parent 19175 | c6e4b073f6a5 |

child 19277 | f7602e74d948 |

1.1 --- a/src/HOL/Set.thy Fri Mar 10 12:28:38 2006 +0100 1.2 +++ b/src/HOL/Set.thy Fri Mar 10 15:33:48 2006 +0100 1.3 @@ -958,7 +958,7 @@ 1.4 outer-level constant, which in this case is just "op :"; we instead need 1.5 to use term-nets to associate patterns with rules. Also, if a rule fails to 1.6 apply, then the formula should be kept. 1.7 - [("uminus", Compl_iff RS iffD1), ("op -", [Diff_iff RS iffD1]), 1.8 + [("HOL.uminus", Compl_iff RS iffD1), ("HOL.minus", [Diff_iff RS iffD1]), 1.9 ("op Int", [IntD1,IntD2]), 1.10 ("Collect", [CollectD]), ("Inter", [InterD]), ("INTER", [INT_D])] 1.11 *)