src/HOL/MetisExamples/Message.thy
2008-05-07 berghofe 2008-05-07 Replaced blast by fast in proof of parts_singleton, since blast looped because of the new encoding of sets.
2007-12-19 paulson 2007-12-19 Replaced refs by config params; finer critical section in mets method
2007-11-23 paulson 2007-11-23 faster metis calls
2007-09-29 wenzelm 2007-09-29 fixed metis proof (Why did it stop working?);
2007-07-11 berghofe 2007-07-11 Adapted to new inductive definition package.
2007-06-21 paulson 2007-06-21 integration of Metis prover