X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=weblib%2FWhile%2Fsemantics.ma;h=ee4362b71ccd197ce70a660c9f8c9b95a27b0d39;hb=569ba7fe357918e3e83c3fe2d5a41070834c5b67;hp=638b7ac912797284c79183abe310d0c5df90d6b1;hpb=4a41f041869956a6c98418e6d06b3a2521a1fb2a;p=helm.git

diff --git a/weblib/While/semantics.ma b/weblib/While/semantics.ma
index 638b7ac91..ee4362b71 100644
--- a/weblib/While/semantics.ma
+++ b/weblib/While/semantics.ma
@@ -14,10 +14,8 @@ definition eqvar ≝ λv1,v2.
 definition update : state → Var → nat → state ≝ λs,v,a,v1. 
   if eqvar v1 v then a else s v1.
 
-
 (* Semantics of Arithmetic expressions *)
-pre class="smallmargin" style="display: inline;"
-let rec evalA a s ≝
+pre class="smallmargin" style="display: inline;"let rec evalA a s ≝
   match a with 
   [ Const n => n
   | Aid v => s v
@@ -30,7 +28,7 @@ let rec evalA a s ≝
  .
 
 example exA1: evalA ((Const 2)+(Const 3)*(Aid (Id 2))) (λx.span style="text-decoration: underline;"1/span) = span style="text-decoration: underline;"5/span.
-normalize // qed. 
+normalize // qed 
 
 let rec evalB b s ≝
   match b with