src/HOL/Quotient_Examples/Quotient_Int.thy
Wed, 11 Jun 2014 14:24:23 +1000 Thomas Sewell Hypsubst preserves equality hypotheses
less more (0) -10 -1 tip