blocking semantic

examples/hoare_logic/blocking_semantics3.mlw

@@ -364,28 +364,28 @@ lemma eval_msubst:
 (*     (eval_fmla sigma pi (subst f x v) <-> *)
 (*      eval_fmla sigma (Cons(x, (get_stack v pi)) pi) f) *)
 
-lemma eval_same_var_term:
-  forall t:term, sigma:env, pi:stack, id:ident, v1 v2:value.
-    eval_term sigma (Cons (id,v1) (Cons (id,v2) pi)) t =
-    eval_term sigma (Cons (id,v1) pi) t
+(* lemma eval_same_var_term: *)
+(*   forall t:term, sigma:env, pi:stack, id:ident, v1 v2:value. *)
+(*     eval_term sigma (Cons (id,v1) (Cons (id,v2) pi)) t = *)
+(*     eval_term sigma (Cons (id,v1) pi) t *)
 
-lemma eval_same_var:
-  forall f:fmla, sigma:env, pi:stack, id:ident, v1 v2:value.
-    eval_fmla sigma (Cons (id,v1) (Cons (id,v2) pi)) f <->
-    eval_fmla sigma (Cons (id,v1) pi) f
+(* lemma eval_same_var: *)
+(*   forall f:fmla, sigma:env, pi:stack, id:ident, v1 v2:value. *)
+(*     eval_fmla sigma (Cons (id,v1) (Cons (id,v2) pi)) f <-> *)
+(*     eval_fmla sigma (Cons (id,v1) pi) f *)
 
 lemma eval_swap_term_any:
-  forall t:term, sigma:env, pi l:stack, id1 id2:ident, v1 v2:value.
-    id1 <> id2 ->
-    (eval_term sigma (l++(Cons (id1,v1) (Cons (id2,v2) pi))) t =
-    eval_term sigma (l++(Cons (id2,v2) (Cons (id1,v1) pi))) t)
+forall t:term, sigma:env, pi l:stack, id1 id2:ident, v1 v2:value.
+id1 <> id2 ->
+(eval_term sigma (l++(Cons (id1,v1) (Cons (id2,v2) pi))) t =
+eval_term sigma (l++(Cons (id2,v2) (Cons (id1,v1) pi))) t)
 
 (* lemma eval_swap_term: *)
 (*   forall t:term, sigma:env, pi:stack, id1 id2:ident, v1 v2:value. *)
 (*     id1 <> id2 -> *)
 (*     (eval_term sigma (Cons (id1,v1) (Cons (id2,v2) pi)) t = *)
 (*     eval_term sigma (Cons (id2,v2) (Cons (id1,v1) pi)) t) *)
-   
+
 lemma eval_swap_any:
   forall f:fmla, sigma:env, pi l:stack, id1 id2:ident, v1 v2:value.
     id1 <> id2 ->