src/HOL/Predicate_Compile_Examples/Specialisation_Examples.thy
Mon, 25 Feb 2013 12:17:50 +0100 wenzelm prefer stateless 'ML_val' for tests;
less more (0) -10 -1 tip