src/HOL/Bali/Trans.thy

   steptr:: "[prog,term \<times> state,term \<times> state] \<Rightarrow> bool" ("_\<turnstile>_ \<mapsto>* _"[61,82,82] 81)
   where "G\<turnstile>p \<mapsto>* p' \<equiv> (p,p') \<in> {(x, y). step G x y}\<^sup>*"
          
 (* Equivalenzen:
   Bigstep zu Smallstep komplett.
-  Smallstep zu Bigstep, nur wenn nicht die Ausdrücke Callee, FinA ,\<dots>
+  Smallstep zu Bigstep, nur wenn nicht die Ausdrücke Callee, FinA ,\<dots>
 *)
 
 (*
 lemma imp_eval_trans:
   assumes eval: "G\<turnstile>s0 \<midarrow>t\<succ>\<rightarrow> (v,s1)" 
     shows trans: "G\<turnstile>(t,s0) \<mapsto>* (\<langle>Lit v\<rangle>,s1)"
 *)
-(* Jetzt muss man bei trans natürlich wieder unterscheiden: Stmt, Expr, Var!
-   Sowas blödes:
+(* Jetzt muss man bei trans natürlich wieder unterscheiden: Stmt, Expr, Var!
+   Sowas blödes:
    Am besten den Terminus ground auf Var,Stmt,Expr hochziehen und dann
    the_vals definieren\<dots>
   G\<turnstile>(t,s0) \<mapsto>* (t',s1) \<and> the_vals t' = v
 *)