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

src/HOL/Set.thy

changeset 34974 | 18b41bba42b5 |

parent 34209 | c7f621786035 |

child 34999 | 5312d2ffee3b |

1.1 --- a/src/HOL/Set.thy Thu Jan 28 11:48:43 2010 +0100 1.2 +++ b/src/HOL/Set.thy Thu Jan 28 11:48:49 2010 +0100 1.3 @@ -928,7 +928,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 - [("HOL.uminus", Compl_iff RS iffD1), ("HOL.minus", [Diff_iff RS iffD1]), 1.8 + [("uminus", Compl_iff RS iffD1), ("minus", [Diff_iff RS iffD1]), 1.9 ("Int", [IntD1,IntD2]), 1.10 ("Collect", [CollectD]), ("Inter", [InterD]), ("INTER", [INT_D])] 1.11 *)