8011
|
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";
|