equal
deleted
inserted
replaced
|
1 (* Title: HOL/MicroJava/J/Prog.ML |
|
2 ID: $Id$ |
|
3 Author: David von Oheimb |
|
4 Copyright 1999 Technische Universitaet Muenchen |
|
5 *) |
|
6 |
|
7 val finite_is_class = prove_goalw thy [is_class_def,class_def,o_def] "finite {C. is_class G C}" (K [ |
|
8 rtac finite_map_of 1]); |
|
9 |
|
10 val is_classI = prove_goalw thy [is_class_def] |
|
11 "\\<And>G. class G C = Some c \\<Longrightarrow> is_class G C" (K [Auto_tac]); |
|
12 |
|
13 val is_classD = prove_goalw thy [is_class_def] |
|
14 "\\<And>G. is_class G C \\<Longrightarrow> \\<exists>sc fs ms. class G C = Some (sc,fs,ms)" (K [ |
|
15 not_None_tac 1, pair_tac "y" 1, pair_tac "ya" 1, Auto_tac]); |