src/HOL/Bali/Trans.thy
changeset 13688 a0b16d42d489
parent 13384 a34e38154413
child 14981 e73f8140af78
--- a/src/HOL/Bali/Trans.thy	Wed Oct 30 12:44:18 2002 +0100
+++ b/src/HOL/Bali/Trans.thy	Thu Oct 31 18:27:10 2002 +0100
@@ -1,6 +1,6 @@
 (*  Title:      HOL/Bali/Trans.thy
     ID:         $Id$
-    Author:     David von Oheimb
+    Author:     David von Oheimb and Norbert Schirmer
     License:    GPL (GNU GENERAL PUBLIC LICENSE)
 
 Operational transition (small-step) semantics of the 
@@ -323,7 +323,7 @@
 Loop: "G\<turnstile>(\<langle>l\<bullet> While(e) c\<rangle>,Norm s) 
         \<mapsto>1 (\<langle>If(e) (Cont l\<bullet>c;; l\<bullet> While(e) c) Else Skip\<rangle>,Norm s)"
 
-Do: "G\<turnstile>(\<langle>Do j\<rangle>,Norm s) \<mapsto>1 (\<langle>Skip\<rangle>,(Some (Jump j), s))"
+Jmp: "G\<turnstile>(\<langle>Jmp j\<rangle>,Norm s) \<mapsto>1 (\<langle>Skip\<rangle>,(Some (Jump j), s))"
 
 ThrowE: "\<lbrakk>G\<turnstile>(\<langle>e\<rangle>,Norm s) \<mapsto>1 (\<langle>e'\<rangle>,s')\<rbrakk> 
          \<Longrightarrow>