[isabelle-dev] find_theorems and type class axioms

Lawrence Paulson lp15 at cam.ac.uk
Mon Nov 16 16:45:58 CET 2015

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?


More information about the isabelle-dev mailing list