1 (* Title: HOL/MicroJava/J/Type.ML
2 ID: $Id$
3 Author: David von Oheimb
4 Copyright 1999 Technische Universitaet Muenchen
5 *)
6
7 Goal "(\\<forall>pt. T \\<noteq> PrimT pt) = (\\<exists>t. T = RefT t)";
8 by(exhaust_tac "T" 1);
9 by Auto_tac;
10 qed "non_PrimT";