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)
Fri, 19 Oct 2012 15:12:52 +0200 webertj Renamed {left,right}_distrib to distrib_{right,left}.
less more (0) -2 tip