src/HOL/MicroJava/BV/LBVCorrect.thy
Thu, 21 Jun 2007 20:07:26 +0200 wenzelm tuned proofs -- avoid implicit prems;
less more (0) -30 -10 -1 tip