src/HOL/MicroJava/J/Type.ML
author nipkow
Thu, 11 Nov 1999 12:23:45 +0100
changeset 8011 d14c4e9e9c8e
child 8423 3c19160b6432
permissions -rw-r--r--
*** empty log message ***
     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";