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}.
Thu, 01 Dec 2011 13:34:12 +0100 blanchet tuning
Tue, 15 Nov 2011 12:39:29 +0100 huffman avoid theorem references like 'semiring_norm(111)'
Mon, 06 Jun 2011 20:36:35 +0200 blanchet tuned Metis examples
less more (0) tip