On 31/08/16 11:04, Burkhart Wolff wrote: > > fun check_hyps context th = > (case undeclared_hyps context th of > [] => th > | undeclared => > error (Pretty.string_of (Pretty.big_list "Undeclared hyps:" > (map (Pretty.item o single o Syntax.pretty_term (Syntax.init_pretty > context)) undeclared))));
Thm.check_hyps is just one more step in tightening the system, to enforce intended logical context structure on tools. It is used in key places where goals and facts are accessed, see Isabelle/625370769fc0 from 11-Jan-2014 (i.e. more than two Isabelle releases ago). Non-compliant tools can use Thm.unchecked_hyps on a local context, but not on a global theory. > A remedy is of course that we manage PO’s fundamentally differently- as terms > with a wrapper that > yields logically true, for instance. This sounds reasonable. Using schematic variables and Logic.mk_term/dest_term or Drule.mk_term/dest_term allows to pass arbitrary term information into and out of goals. See also the "implementation" manual, section 2.3.2. > Another way is of course to define our own command thm, of course, without > the check. This would mean to work against the overall system infrastructure. It is unlikely to work out properly. > Still, we think that the generation of PO’s via Thm.assume is conceptually > the cleanest way. Maybe in a version of Isabelle from more 10-15 years ago. The context has become very important after 2005, and more and more explicit checks have emerged. > isabelle-dev mailing list BTW, the front page defines this mailing list as follows: "covers the Isabelle development process, including intermediate repository versions, and administrative issues concerning the website or testing infrastructure." Almost everything else should go to isabelle-users. Using Isabelle/ML for Isabelle tool development is normal use of Isabelle, not development of Isabelle itself. Makarius _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev