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
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
