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