src/HOL/Nominal/Examples/Crary.thy
Wed, 28 Mar 2007 01:55:18 +0200 urbanc tuned proofs (taking full advantage of nominal_inductive)
less more (0) -1 tip