| Thu, 14 Apr 2011 11:24:05 +0200 | blanchet | handle case where the same Skolem name is given different types in different subgoals in the new Skolemizer (this can happen if several type-instances of the same fact are needed by Metis, cf. example in "Clausify.thy") -- the solution reintroduces old code removed in a6725f293377 | changeset | files |
| Thu, 14 Apr 2011 11:24:04 +0200 | blanchet | removed obsolete Skolem counter in new Skolemizer | changeset | files |