src/HOL/Metis_Examples/Clausify.thy
2011-05-12 blanchet 2011-05-12 use the same code for extensionalization in Metis and Sledgehammer and generalize that code so that it gracefully handles negations (e.g. negated conjecture), formulas of the form (%x. t) = u, etc.
2011-04-14 blanchet 2011-04-14 more clausification tests
2011-04-14 blanchet 2011-04-14 added examples of definitional CNF facts
2011-04-14 blanchet 2011-04-14 compile
2011-04-14 blanchet 2011-04-14 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
2011-04-14 blanchet 2011-04-14 added outstanding issue to Metis example
2011-04-14 blanchet 2011-04-14 started clausifier examples