src/HOL/Code_Evaluation.thy
Tue, 01 Sep 2015 22:32:58 +0200 wenzelm eliminated \<Colon>;
less more (0) -30 -10 -1 tip