src/HOL/Bali/Trans.thy
changeset 40945 b8703f63bfb2
parent 37956 ee939247b2fb
child 47176 568fdc70e565
     1.1 --- a/src/HOL/Bali/Trans.thy	Fri Dec 03 20:26:57 2010 +0100
     1.2 +++ b/src/HOL/Bali/Trans.thy	Fri Dec 03 20:38:58 2010 +0100
     1.3 @@ -364,7 +364,7 @@
     1.4           
     1.5  (* Equivalenzen:
     1.6    Bigstep zu Smallstep komplett.
     1.7 -  Smallstep zu Bigstep, nur wenn nicht die Ausdrücke Callee, FinA ,\<dots>
     1.8 +  Smallstep zu Bigstep, nur wenn nicht die Ausdrücke Callee, FinA ,\<dots>
     1.9  *)
    1.10  
    1.11  (*
    1.12 @@ -372,8 +372,8 @@
    1.13    assumes eval: "G\<turnstile>s0 \<midarrow>t\<succ>\<rightarrow> (v,s1)" 
    1.14      shows trans: "G\<turnstile>(t,s0) \<mapsto>* (\<langle>Lit v\<rangle>,s1)"
    1.15  *)
    1.16 -(* Jetzt muss man bei trans natürlich wieder unterscheiden: Stmt, Expr, Var!
    1.17 -   Sowas blödes:
    1.18 +(* Jetzt muss man bei trans natürlich wieder unterscheiden: Stmt, Expr, Var!
    1.19 +   Sowas blödes:
    1.20     Am besten den Terminus ground auf Var,Stmt,Expr hochziehen und dann
    1.21     the_vals definieren\<dots>
    1.22    G\<turnstile>(t,s0) \<mapsto>* (t',s1) \<and> the_vals t' = v