src/HOL/Metis_Examples/Binary_Tree.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)
less more (0) -1 tip