# HG changeset patch
# User wenzelm
# Date 1214424095 -7200
# Node ID 6d93bbe5633e53ce713d06d0f5b8c6a0d4770804
# Parent  a6dc1769fdda19ae693f4ac5a20401644e74e4c3
tuned proofs;

diff -r a6dc1769fdda -r 6d93bbe5633e src/HOL/IMP/Compiler0.thy
--- a/src/HOL/IMP/Compiler0.thy	Wed Jun 25 22:01:34 2008 +0200
+++ b/src/HOL/IMP/Compiler0.thy	Wed Jun 25 22:01:35 2008 +0200
@@ -71,13 +71,13 @@
 lemma app_right_1:
   assumes "is1 \<turnstile> \<langle>s1,i1\<rangle> -1\<rightarrow> \<langle>s2,i2\<rangle>"
   shows "is1 @ is2 \<turnstile> \<langle>s1,i1\<rangle> -1\<rightarrow> \<langle>s2,i2\<rangle>"
-  using prems
+  using assms
   by induct auto
 
 lemma app_left_1:
   assumes "is2 \<turnstile> \<langle>s1,i1\<rangle> -1\<rightarrow> \<langle>s2,i2\<rangle>"
   shows "is1 @ is2 \<turnstile> \<langle>s1,size is1+i1\<rangle> -1\<rightarrow> \<langle>s2,size is1+i2\<rangle>"
-  using prems
+  using assms
   by induct auto
 
 declare rtrancl_induct2 [induct set: rtrancl]
@@ -85,7 +85,7 @@
 lemma app_right:
   assumes "is1 \<turnstile> \<langle>s1,i1\<rangle> -*\<rightarrow> \<langle>s2,i2\<rangle>"
   shows "is1 @ is2 \<turnstile> \<langle>s1,i1\<rangle> -*\<rightarrow> \<langle>s2,i2\<rangle>"
-  using prems
+  using assms
 proof induct
   show "is1 @ is2 \<turnstile> \<langle>s1,i1\<rangle> -*\<rightarrow> \<langle>s1,i1\<rangle>" by simp
 next
@@ -99,7 +99,7 @@
 lemma app_left:
   assumes "is2 \<turnstile> \<langle>s1,i1\<rangle> -*\<rightarrow> \<langle>s2,i2\<rangle>"
   shows "is1 @ is2 \<turnstile> \<langle>s1,size is1+i1\<rangle> -*\<rightarrow> \<langle>s2,size is1+i2\<rangle>"
-using prems
+using assms
 proof induct
   show "is1 @ is2 \<turnstile> \<langle>s1,length is1 + i1\<rangle> -*\<rightarrow> \<langle>s1,length is1 + i1\<rangle>" by simp
 next
@@ -119,7 +119,7 @@
   assumes "is \<turnstile> \<langle>s1,i1\<rangle> -*\<rightarrow> \<langle>s2,i2\<rangle>"
   shows "instr # is \<turnstile> \<langle>s1,Suc i1\<rangle> -*\<rightarrow> \<langle>s2,Suc i2\<rangle>"
 proof -
-  from app_left [OF prems, of "[instr]"]
+  from app_left [OF assms, of "[instr]"]
   show ?thesis by simp
 qed
 
@@ -136,7 +136,7 @@
 theorem
   assumes "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c t"
   shows "compile c \<turnstile> \<langle>s,0\<rangle> -*\<rightarrow> \<langle>t,length(compile c)\<rangle>" (is "?P c s t")
-  using prems
+  using assms
 proof induct
   show "\<And>s. ?P \<SKIP> s s" by simp
 next