src/HOL/Metis_Examples/Message.thy
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)
Mon, 02 Jan 2012 14:45:13 +0100 blanchet reintroduced "metis" call taken out after reintroducing "set" as a constructor, and added two "metis" calls that used to be too slow
Sat, 24 Dec 2011 15:53:10 +0100 haftmann adjusted to set/pred distinction by means of type constructor `set`
Sun, 20 Nov 2011 21:05:23 +0100 wenzelm eliminated obsolete "standard";
less more (0) -10 -4 tip