Am 12.02.2014 um 19:40 schrieb Makarius <makar...@sketis.net>: > In principle the concept of "bound" variable in the context can do that, see > also Variable.next_bound. It enumerates local variables in a way such that > the usual term order (the one of the Simplifier) coincides with the > enumeration order.
Good to know. I might end up using it. >> Metis is a FO ATP developed by Hurd. "metis" is a higher-order proof method >> (and tactic) that translates HOL to FOL (like Sledgehammer does), developed >> by Paulson & Susanto. > > Do you understand yourself how that works? Does "that" refer to Metis or "metis"? I've never looked much under Metis's hood except to tweak its options. For "metis", the answer is a qualified yes. Jasmin _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
