src/HOL/Isar_examples/ExprCompiler.thy
Wed, 13 Jun 2007 18:30:11 +0200 wenzelm tuned proofs: avoid implicit prems;
Wed, 13 Sep 2006 12:05:50 +0200 krauss Major update to function package, including new syntax and the (only theoretical)
Mon, 11 Sep 2006 21:35:19 +0200 wenzelm induct method: renamed 'fixing' to 'arbitrary';
Wed, 16 Nov 2005 19:34:19 +0100 wenzelm tuned document;
less more (0) -30 -10 -4 tip