> On 26 Nov 2015, at 11:58, Florian Haftmann
> <florian.haftm...@informatik.tu-muenchen.de> wrote:
>
> The sort constraints of constants play *no* role for
> searching theorems. The sort constraints of terms to be searched *do*,
> and in my view this is the desired behaviour: if I formulate a property
> on partial orders, I do not want to be bothered by facts which only
> apply to linear orders.
I’m not sure that I understand this statement. At what point do constants
become terms anyway? Consider the following search:
"_<=_" "_=_”
There are two terms, but they are nothing but constants. No theory is implied
(I’m not sure how one could express a search that was specifically about
partial orders that were not linear), and there are more than 2000 hits. They
include statements involving natural numbers, integers and sets. In fact it
would be good to find a way of excluding some of those.
Meanwhile, the search
norm dist
contains only constants, and nevertheless it fails to pick up dist_norm: "dist
x y = norm (x - y)”.
Larry
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
