src/HOL/Tools/Function/partial_function.ML
Fri, 22 Mar 2013 00:39:14 +0100 krauss allow induction predicates with arbitrary arity (not just binary)
less more (0) -10 -1 tip