src/HOL/FunDef.thy
Fri, 24 Nov 2006 13:44:51 +0100 krauss Lemma "fundef_default_value" uses predicate instead of set.
less more (0) -10 -1 tip