Talk:Event-B Language

From Event-B
Revision as of 12:21, 27 October 2009 by imported>Tianhaiyun (The problem encountered when using Rodin.)
(diff) ← Older revision | Latest revision (diff) | Newer revision → (diff)
Jump to navigationJump to search
The printable version is no longer supported and may have rendering errors. Please update your browser bookmarks and please use the default browser print function instead.

Rodin Platform Version: 0.9.1

Sequent Prover Auto-tactic : all

The problems is as follows. I build one project, in which there is only one context. In this contest, there is only one theorem defined as {x·x∈0‥4∣x↦0}∈0‥4⇸0‥4. The obligation for it is generated by Rodin. However, it reports that the obligation can cannot be passed. It makes me quite confused. Please everyone knowing what the problem is and help me out.

Thank you so lot

HaiYun tian SCM Teesside University