--- a/src/HOL/MicroJava/BV/BVExample.thy Sat May 19 11:33:25 2007 +0200
+++ b/src/HOL/MicroJava/BV/BVExample.thy Sat May 19 11:33:26 2007 +0200
@@ -5,7 +5,9 @@
header {* \isaheader{Example Welltypings}\label{sec:BVExample} *}
-theory BVExample imports JVMListExample BVSpecTypeSafe JVM ExecutableSet begin
+theory BVExample
+imports JVMListExample BVSpecTypeSafe JVM ExecutableSet
+begin
text {*
This theory shows type correctness of the example program in section
@@ -115,7 +117,7 @@
lemma field_val [simp]:
"field (E, list_name) val_name = Some (list_name, PrimT Integer)"
- apply (unfold field_def)
+ apply (unfold TypeRel.field_def)
apply (insert class_list)
apply (unfold list_class_def)
apply (drule fields_rec_lemma [OF _ wf_subcls1_E])
@@ -124,7 +126,7 @@
lemma field_next [simp]:
"field (E, list_name) next_name = Some (list_name, Class list_name)"
- apply (unfold field_def)
+ apply (unfold TypeRel.field_def)
apply (insert class_list)
apply (unfold list_class_def)
apply (drule fields_rec_lemma [OF _ wf_subcls1_E])
--- a/src/HOL/MicroJava/Comp/CorrCompTp.thy Sat May 19 11:33:25 2007 +0200
+++ b/src/HOL/MicroJava/Comp/CorrCompTp.thy Sat May 19 11:33:26 2007 +0200
@@ -1237,7 +1237,7 @@
apply simp+
apply (simp only: comp_is_type)
apply (rule_tac C=cname in fields_is_type)
-apply (simp add: field_def)
+apply (simp add: TypeRel.field_def)
apply (drule JBasis.table_of_remap_SomeD)+
apply assumption+
apply (erule wf_prog_ws_prog)
--- a/src/HOL/MicroJava/Comp/LemmasComp.thy Sat May 19 11:33:25 2007 +0200
+++ b/src/HOL/MicroJava/Comp/LemmasComp.thy Sat May 19 11:33:26 2007 +0200
@@ -5,7 +5,9 @@
(* Lemmas for compiler correctness proof *)
-theory LemmasComp imports TranslComp begin
+theory LemmasComp
+imports TranslComp
+begin
declare split_paired_All [simp del]
@@ -222,7 +224,7 @@
lemma comp_field: "wfP ((subcls1 G)^--1) \<Longrightarrow>
field (comp G,C) = field (G,C)"
-by (simp add: field_def comp_fields)
+by (simp add: TypeRel.field_def comp_fields)