Andreas’s message reminds me that axioms of type classes are still not picked up: class dist_norm = dist + norm + minus + assumes dist_norm: "dist x y = norm (x - y)” This item has the status of a theorem. However, the query dist "norm(_-_)” doesn’t find it. Surely it should? Larry