src/HOL/Auth/Message.thy
Wed, 21 Jul 1999 15:22:11 +0200 paulson tweaked proofs to handle new freeness reasoning for data c onstructors
less more (0) -10 -1 tip