isabelle: File revisions

src/HOL/Metis_Examples/Clausification.thy

Sun, 02 Nov 2014 18:21:45 +0100	wenzelm	modernized header uniformly as section;	file \| diff \| annotate
Wed, 12 Feb 2014 08:37:06 +0100	blanchet	adapted to 'xxx_{case,rec}' renaming, to new theorem names, and to new variable names in theorems	file \| diff \| annotate
Thu, 03 Jan 2013 17:28:55 +0100	blanchet	use new skolemizer for reconstructing skolemization steps in Isar proofs (because the old skolemizer messes up the order of the Skolem arguments)	file \| diff \| annotate
Thu, 03 Jan 2013 13:28:37 +0100	blanchet	get rid of two-year-old hack, now that the "metis" skolemizer no longer gets stuck in HO unification	file \| diff \| annotate
Tue, 03 Apr 2012 16:26:48 +0200	kuncar	new package Lifting - initial commit	file \| diff \| annotate
Tue, 07 Jun 2011 08:52:35 +0200	blanchet	obsoleted "metisFT", and added "no_types" version of Metis as fallback to Sledgehammer after noticing how useful it can be	file \| diff \| annotate
Mon, 06 Jun 2011 20:36:35 +0200	blanchet	tuned Metis examples	file \| diff \| annotate \| base

isabelle