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   *)