src/HOL/MicroJava/J/Example.thy
Tue, 13 Oct 2015 09:21:15 +0200 haftmann prod_case as canonical name for product type eliminator
less more (0) -30 -10 -1 tip