src/HOL/Predicate.thy
Sat, 24 Dec 2011 15:53:10 +0100 haftmann adjusted to set/pred distinction by means of type constructor `set`
Fri, 25 Nov 2011 13:14:58 +0100 wenzelm proper intro? declarations -- NB: elim? indexes on major premise, which is too flexible here and easily leads to inefficiences (cf. a0336f8b6558);
less more (0) -30 -10 -2 tip