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/Small_Step.thy
changeset 45265 521508e85c0d
parent 45218 f115540543d8
child 45415 bf39b07a7a8e 
--- a/src/HOL/IMP/Small_Step.thy	Tue Oct 25 12:00:52 2011 +0200
+++ b/src/HOL/IMP/Small_Step.thy	Tue Oct 25 15:59:15 2011 +0200
@@ -114,7 +114,7 @@
   let ?if = "IF b THEN c; WHILE b DO c ELSE SKIP"
   have "(WHILE b DO c,s) \<rightarrow> (?if, s)" by blast
   moreover have "(?if,s) \<rightarrow> (SKIP, s)" by (simp add: b)
-  ultimately show "(WHILE b DO c,s) \<rightarrow>* (SKIP,s)" by (metis refl step)
+  ultimately show "(WHILE b DO c,s) \<rightarrow>* (SKIP,s)" by(metis star.refl star.step)
 next
   fix b c s s' t
   let ?w  = "WHILE b DO c"
@@ -137,16 +137,16 @@
 next
   case Semi thus ?case by (blast intro: semi_comp)
 next
-  case IfTrue thus ?case by (blast intro: step)
+  case IfTrue thus ?case by (blast intro: star.step)
 next
-  case IfFalse thus ?case by (blast intro: step)
+  case IfFalse thus ?case by (blast intro: star.step)
 next
   case WhileFalse thus ?case
-    by (metis step step1 small_step.IfFalse small_step.While)
+    by (metis star.step star_step1 small_step.IfFalse small_step.While)
 next
   case WhileTrue
   thus ?case
-    by(metis While semi_comp small_step.IfTrue step[of small_step])
+    by(metis While semi_comp small_step.IfTrue star.step[of small_step])
 qed
 
 lemma small1_big_continue:
isabelle