Hi Makarius, > On 10 May 2016, at 22:48, Makarius <makar...@sketis.net> wrote: > > On 03/03/16 14:19, Dmitriy Traytel wrote: > >> I wondered whether named_theorems (or more generally all dynamic facts) >> deserve to be more visible. In particular when I search for >> >> "(?a < ?c - ?b) = (?a + ?b < ?c)” >> >> with find_theorems, I’d like to be reminded of algebra_simps (instead or >> rather in addition to Groups.ordered_ab_group_add_class.less_diff_eq). >> >> Looking at the named_theorems that we have today (with grep), I see two >> kinds: those relevant for the working formalizer (algebra_simps, >> derivative_intros, ...), and those mostly relevant for tools (transfer_raw, >> …). It would be good to make the former ones easily discoverable (via >> find_theorems, potentially also Sledgehammer). If something is really >> irrelevant for the working formalizer, it(s binding) could in principle be >> concealed (preventing find_theorems from showing it). > > See now the following change: > > changeset: 63080:8326aa594273 > tag: tip > user: wenzelm > date: Tue May 10 22:25:06 2016 +0200 > files: src/Pure/Isar/proof_context.ML > src/Pure/Tools/find_theorems.ML src/Pure/facts.ML > description: > find dynamic facts as well, but static ones are preferred; > tuned; > > > It is not precisely what you have described, but it is a > straight-forward continuation of the existing fact retrieval. > > Note that the "Duplicates" option makes a difference if dynamic facts > actually show up. The details of these policies are from a different > continent, and not totally clear to me. > >> PS: The real reason why I am interested in this is that in the forthcoming >> package for non-primitive corecursion (joint work with Jasmin Blanchette, >> Aymeric Bouzy, Andreas Lochbihler, Andrei Popescu), we would like to >> generate dynamic theorems for coinduction up to congruence (because the >> coinduction principles gets stronger with every non-primitively corecursive >> function defined). But this only makes sense if users are aware of those >> dynamic theorems, i.e. can find them easily. > > Is the above sufficient for this application?
Yes, thanks! Ticking “Duplicates” makes the result even more as I expected. But I can imagine that showing no duplicates (with static theorems preferred) is a reasonable default. Dmitriy _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
