isabelle: File revisions

src/HOL/Metis_Examples/Clausify.thy

Thu, 12 May 2011 15:29:19 +0200	blanchet	added two mildly higher-order examples contributed by TN, removed references to obsoleted type systems, and moved things around	file \| diff \| annotate
Thu, 12 May 2011 15:29:19 +0200	blanchet	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.	file \| diff \| annotate
Thu, 14 Apr 2011 11:24:05 +0200	blanchet	more clausification tests	file \| diff \| annotate
Thu, 14 Apr 2011 11:24:05 +0200	blanchet	added examples of definitional CNF facts	file \| diff \| annotate
Thu, 14 Apr 2011 11:24:05 +0200	blanchet	compile	file \| diff \| annotate
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	file \| diff \| annotate
Thu, 14 Apr 2011 11:24:04 +0200	blanchet	added outstanding issue to Metis example	file \| diff \| annotate
Thu, 14 Apr 2011 11:24:04 +0200	blanchet	started clausifier examples	file \| diff \| annotate

isabelle