Perhaps the question relates to how polymorphism is interpreted in these searches. I’m getting the idea that the search for “dist” and “norm” somehow produces a combination of type classes that doesn’t precisely match the instances in the axiom “dist_norm”, where they are too specific to be picked up. And yet, searching for “op<“ picks up a lot of theorems about natural numbers even though the original search is polymorphic. So it may be that our interpretation of “too specific” needs to be revisited.
Larry > On 22 Dec 2015, at 08:38, Florian Haftmann > <florian.haftm...@informatik.tu-muenchen.de> wrote: > > I think the misunderstanding is that »find_theorems foo« searches for > theorems containing a constant named »foo«. This is not the case – it > searches for theorems containing a subterm matching »foo«. I guess it > would be possible to implement searching for constants as a separate > criterion; this could also ignore sort constraints in the first place. > > Cheers, > Florian > >> >> Larry _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
