src/HOL/Quotient_Examples/Quotient_Int.thy
Tue, 09 Nov 2010 14:02:14 +0100 haftmann fun_rel_def is no simp rule by default
less more (0) -1 tip