-
The new preference about section expansion does not improve matters.
2010-01-06 18:00:12 UTC by nicolas_beauger
-
Fixed New actions in proving perspective.
Fixed pre-fill of project name in new component wizard.
Committed to Subversion (r8010, r8011, r8013).
However, there are still some minor problems left:
- the new action in the contextual menu of a project in the Event-B explorer doesn't emphasize "New Event-B Component" and "New Event-B Project" (one still has to click on Other...)
-...
2010-01-06 11:30:12 UTC by thomasmuller
-
The simple case {E |-> F}[T] == X actually yields several cases, depending on the hypotheses we have at hand:
. if T is a type then the SIMP_TYPE_RELIMAGE rule applies and X = ran({E |-> F})
. E : T => X = F
. E /: T => X = {}
. no hyp => X cannot be determined, thus no rewrite occurs
In the general case {E1 |-> F1, ..., En |-> Fn}[T] == X, these cases must be reformulated:
. if T is...
2010-01-06 10:35:24 UTC by nicolas_beauger
-
Did not reproduce the NoSuchMethodError problem with Rodin / Eclipse 3.5.
Uploaded an updated version of the sample project: removed the remainings of c0 and updated with new AnimB syntax.
2010-01-05 14:16:55 UTC by nicolas_beauger
-
The 'pretty print' view of the Event-B editor should reflect extensions made to the editor by plug-ins.
Similarly, the other views of the editor (tree structured edit views)
2010-01-05 13:40:56 UTC by cfsnook
-
If we have the 2 hypos:
a
2009-12-28 15:09:42 UTC by tshoang
-
It might be useful to have a rule in order to be proposed a proof by cases with hypo
a
2009-12-28 15:06:09 UTC by tshoang
-
I've an hypo such f : 1..k >->> s (then f~:s>->>1..k) it can be
convenient to obtain the hypo card(s)=k.
In other cases we have card(s)=k in the set of hypos. can we have
#f.f:s>->>1..k as a new hypo.
(This request is from Dominique Cansell via private communication)
2009-12-28 15:01:45 UTC by tshoang
-
It turns out that the rule proposed is not correct
r1 \/ r2 \/ ... : S r1 : S & r2 : S & ...
A counter example is S = {{x} | x : NAT}, r1 = {1}, r2 = {2}
The correct rule is
r1 \/ r2 \/ ... : POW(S) r1 : POW(S) & r2 : POW(S) & ...
2009-12-28 14:57:46 UTC by tshoang
-
The dual rule is as follows:
e : S1 /\ ... /\ S2 e:S1 & ... & e:S2
(This request is by Jean-Raymond Abrial via private communication)
2009-12-28 14:51:16 UTC by tshoang
