Commit 219a32e2 authored by charguer's avatar charguer

tests

parent 30e62e96
......@@ -1620,6 +1620,14 @@ Qed.
Arguments normally_hwand : clear implicits.
(* ---------------------------------------------------------------------- *)
(*
Definition ROFrame H1 H2 :=
Hexists H, normally H \* (RO H \--* H1) \* normally (H \--* H2).
......@@ -1644,12 +1652,6 @@ Abort.
(* ---------------------------------------------------------------------- *)
(*
Definition ROFrame' H1 H2 :=
Hexists H, normally H2 \* (RO H \--* H1) \* (H \--* H2).
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment