Nobody has commented on this issue, and I would like to re-raise it, as it affects the development version.
It simply doesn’t make sense that fundamental axioms such as dist_norm are concealed from find_theorems. I imagine it would be very easy to change this behaviour. Larry > Begin forwarded message: > > From: Larry Paulson <l...@cam.ac.uk> > Subject: Re: [isabelle] find_theorems and locales > Date: 19 June 2015 16:22:53 BST > To: Florian Haftmann <florian.haftm...@informatik.tu-muenchen.de> > Cc: Bertram Felgenhauer <bertram.felgenha...@googlemail.com>, > cl-isabelle-us...@lists.cam.ac.uk > > I've stumbled across a related issue with find_theorems that certainly seems > wrong. I was searching for the theorem > Real_Vector_Spaces.dist_norm_class.dist_norm, which is introduced as a type > class axiom here: > > class dist_norm = dist + norm + minus + > assumes dist_norm: "dist x y = norm (x - y)" > > Calling find_theorems with suitable patterns, such as > > dist "norm (_-_)” > > does not return this theorem among the results, but clearly it should. > > Larry _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
