src/HOL/Isar_examples/ExprCompiler.thy
Wed, 13 Jun 2007 18:30:11 +0200 wenzelm tuned proofs: avoid implicit prems;
less more (0) -30 -10 -1 tip