# HG changeset patch
# User nipkow
# Date 944486625 -3600
# Node ID b7f7e18eb58494d8e61e8c57fbbbd71e21001593
# Parent  3a0c996cf2b2a3dc46f0ca57058c7f0d7076d167
Renamed some vars

diff -r 3a0c996cf2b2 -r b7f7e18eb584 src/HOL/MicroJava/BV/BVSpec.thy
--- a/src/HOL/MicroJava/BV/BVSpec.thy	Thu Dec 02 09:09:30 1999 +0100
+++ b/src/HOL/MicroJava/BV/BVSpec.thy	Mon Dec 06 14:23:45 1999 +0100
@@ -188,10 +188,10 @@
 
 
  wt_method :: "[jvm_prog,cname,ty list,ty,nat,instr list,method_type] \\<Rightarrow> bool"
- "wt_method G cn pTs rT mxl ins phi \\<equiv>
+ "wt_method G C pTs rT mxl ins phi \\<equiv>
 	let max_pc = length ins
         in
-	0 < max_pc \\<and> wt_start G cn pTs mxl phi \\<and> 
+	0 < max_pc \\<and> wt_start G C pTs mxl phi \\<and> 
 	(\\<forall>pc. pc<max_pc \\<longrightarrow> wt_instr (ins ! pc) G rT phi max_pc pc)"
 
  wt_jvm_prog :: "[jvm_prog,prog_type] \\<Rightarrow> bool"
diff -r 3a0c996cf2b2 -r b7f7e18eb584 src/HOL/MicroJava/BV/BVSpecTypeSafe.ML
--- a/src/HOL/MicroJava/BV/BVSpecTypeSafe.ML	Thu Dec 02 09:09:30 1999 +0100
+++ b/src/HOL/MicroJava/BV/BVSpecTypeSafe.ML	Mon Dec 06 14:23:45 1999 +0100
@@ -607,8 +607,8 @@
 
 
 Goal
-"\\<lbrakk> wt_jvm_prog G phi; G \\<turnstile> s0 -jvm\\<rightarrow> (None,hp,(stk,loc,cn,sig,pc)#frs); G,phi \\<turnstile>JVM s0 \\<surd>\\<rbrakk> \
-\ \\<Longrightarrow>  approx_stk G hp stk (fst (((phi  cn)  sig) ! pc)) \\<and> approx_loc G hp loc (snd (((phi  cn)  sig) ! pc)) ";
+"\\<lbrakk> wt_jvm_prog G phi; G \\<turnstile> s0 -jvm\\<rightarrow> (None,hp,(stk,loc,C,sig,pc)#frs); G,phi \\<turnstile>JVM s0 \\<surd>\\<rbrakk> \
+\ \\<Longrightarrow>  approx_stk G hp stk (fst (((phi  C)  sig) ! pc)) \\<and> approx_loc G hp loc (snd (((phi  C)  sig) ! pc)) ";
 bd BV_correct 1;
 ba 1;
 ba 1;
diff -r 3a0c996cf2b2 -r b7f7e18eb584 src/HOL/MicroJava/BV/Correct.ML
--- a/src/HOL/MicroJava/BV/Correct.ML	Thu Dec 02 09:09:30 1999 +0100
+++ b/src/HOL/MicroJava/BV/Correct.ML	Mon Dec 06 14:23:45 1999 +0100
@@ -17,7 +17,7 @@
 
 
 Goalw [hext_def]
-"hp a = Some (cn,od') \\<longrightarrow> hp \\<le>| (hp(a \\<mapsto> (cn,od)))";
+"hp a = Some (C,od') \\<longrightarrow> hp \\<le>| (hp(a \\<mapsto> (C,od)))";
 by (asm_full_simp_tac (simpset() addsimps []) 1);
 qed_spec_mp "sup_heap_update_value";
 
@@ -254,9 +254,9 @@
 Delsimps [fun_upd_apply]; 
 Goal
 "\\<forall>rT C sig. correct_frames G hp phi rT sig frs \\<longrightarrow> \
-\    hp a = Some (cn,od) \\<longrightarrow> map_of (fields (G, cn)) fl = Some fd \\<longrightarrow> \
+\    hp a = Some (C,od) \\<longrightarrow> map_of (fields (G, C)) fl = Some fd \\<longrightarrow> \
 \    G,hp\\<turnstile>v\\<Colon>\\<preceq>fd \
-\ \\<longrightarrow> correct_frames G (hp(a \\<mapsto> (cn, od(fl\\<mapsto>v)))) phi rT sig frs";
+\ \\<longrightarrow> correct_frames G (hp(a \\<mapsto> (C, od(fl\\<mapsto>v)))) phi rT sig frs";
 by (induct_tac "frs" 1);
  by (Asm_full_simp_tac 1);
 by (asm_full_simp_tac (simpset() addsimps [split_def,correct_frame_def]) 1);
diff -r 3a0c996cf2b2 -r b7f7e18eb584 src/HOL/MicroJava/JVM/Method.thy
--- a/src/HOL/MicroJava/JVM/Method.thy	Thu Dec 02 09:09:30 1999 +0100
+++ b/src/HOL/MicroJava/JVM/Method.thy	Mon Dec 06 14:23:45 1999 +0100
@@ -40,7 +40,7 @@
 primrec
   "exec_mr Return stk0 frs =
 	(if frs=[] then []
-         else let val = hd stk0; (stk,loc,cn,met,pc) = hd frs
-	      in (val#stk,loc,cn,met,pc)#tl frs)"
+         else let val = hd stk0; (stk,loc,C,sig,pc) = hd frs
+	      in (val#stk,loc,C,sig,pc)#tl frs)"
 
 end