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/Bali/Trans.thy
changeset 40945 b8703f63bfb2
parent 37956 ee939247b2fb
child 47176 568fdc70e565 
--- a/src/HOL/Bali/Trans.thy	Fri Dec 03 20:26:57 2010 +0100
+++ b/src/HOL/Bali/Trans.thy	Fri Dec 03 20:38:58 2010 +0100
@@ -364,7 +364,7 @@
          
 (* 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>
 *)
 
 (*
@@ -372,8 +372,8 @@
   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
isabelle