Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/IMP/Transition.thy
changeset 41529 ba60efa2fd08
parent 34990 81e8fdfeb849 
--- a/src/HOL/IMP/Transition.thy	Wed Jan 12 17:14:27 2011 +0100
+++ b/src/HOL/IMP/Transition.thy	Wed Jan 12 17:19:50 2011 +0100
@@ -272,7 +272,7 @@
 lemma evalc_imp_evalc1:
   assumes "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s'"
   shows "\<langle>c, s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s'\<rangle>"
-  using prems
+  using assms
 proof induct
   fix s show "\<langle>\<SKIP>,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s\<rangle>" by auto
 next
@@ -550,7 +550,7 @@
   shows "\<langle>c1;c2,s1\<rangle> \<longrightarrow>\<^sub>1\<^sup>* cs3"
 proof -
   -- {* The induction rule needs @{text P} to be a function of @{term "Some c1"} *}
-  from prems
+  from assms
   have "\<langle>(\<lambda>c. if c = None then c2 else the c; c2) (Some c1),s1\<rangle> \<longrightarrow>\<^sub>1\<^sup>* cs3"
     apply (induct rule: converse_rtrancl_induct2)
      apply simp
isabelle