Relation Rewrite Rules: Revision history

3 June 2024

• curprev 15:1315:13, 3 June 2024‎ Guillaume talk contribs‎ 33,658 bytes +1‎ Rules DEF_EQUAL_FUN_IMAGE and SIMP_SPECIAL_IN_*ID have been implemented in Rodin 3.9

8 March 2024

• curprev 16:1716:17, 8 March 2024‎ Guillaume talk contribs‎ 33,657 bytes +538‎ Add four rules related to set membership and identity

5 February 2024

• curprev 14:3114:31, 5 February 2024‎ Guillaume talk contribs‎ 33,119 bytes +110‎ Add rule DEF_EQUAL_FUNIMAGE

6 April 2023

• curprev 09:3209:32, 6 April 2023‎ Guillaume talk contribs‎ 33,009 bytes +1‎ Rule DEF_BCOMP has been implemented in Rodin 3.8

19 February 2014

• curprev 16:4516:45, 19 February 2014‎ imported>Laurent‎ 33,008 bytes 0‎ mark rules as implemented

18 February 2014

• curprev 09:3009:30, 18 February 2014‎ imported>Laurent‎ 33,008 bytes +211‎ Add rule about properties of identity.
• curprev 09:2509:25, 18 February 2014‎ imported>Laurent‎ 32,797 bytes +372‎ Refactor rules about projections

2 May 2013

• curprev 15:2315:23, 2 May 2013‎ imported>Josselin‎ 32,425 bytes −362‎ Removed rules SIMP_SPECIAL_EQUAL_REL and SIMP_SPECIAL_EQUAL_RELDOM (moved to Empty Set Rewrite Rules)

26 April 2013

• curprev 13:3313:33, 26 April 2013‎ imported>Laurent‎ 32,787 bytes −22‎ FIx incorrect rule SIMP_SPECIAL_EQUAL_RELDOM (see bug #661)

30 September 2011

• curprev 12:4812:48, 30 September 2011‎ imported>Billaude‎ 32,809 bytes −460‎ The four last rules already exist, but were not implemented. Instead of being manual, they are automatic.

28 September 2011

• curprev 15:2515:25, 28 September 2011‎ imported>Billaude‎ 33,269 bytes +1,057‎ Adding 9 new rewriting rules.

19 July 2011

• curprev 16:2416:24, 19 July 2011‎ imported>Laurent‎ 32,212 bytes +472‎ Added rules SIMP_MULTI_DOM_DOMRES, SIMP_MULTI_DOM_DOMSUB, SIMP_MULTI_RAN_RANRES, SIMP_MULTI_RAN_RANSUB

4 April 2011

• curprev 15:2415:24, 4 April 2011‎ imported>Laurent‎ 31,740 bytes +134‎ Added rule DERIV_FCOMP_SING

17 January 2011

• curprev 17:3217:32, 17 January 2011‎ imported>Benoit‎ m 31,606 bytes +2‎ Added stars to the automatic rules implemented in auto rewriter L2.
• curprev 17:1917:19, 17 January 2011‎ imported>Benoit‎ m 31,604 bytes +15‎ Added stars to the automatic rules implemented in auto rewriter L2.
• curprev 17:0117:01, 17 January 2011‎ imported>Benoit‎ m 31,589 bytes +51‎ Added stars to the automatic rules implemented in auto rewriter L2.

14 January 2011

• curprev 09:1309:13, 14 January 2011‎ imported>Benoit‎ 31,538 bytes +123‎ Added rule SIMP_RELIMAGE_DOMSUB_ID

13 January 2011

• curprev 16:3216:32, 13 January 2011‎ imported>Benoit‎ m 31,415 bytes +2‎ Renamed SIMP_RELIMAGE_ID in SIMP_RELIMAGE_DOMRES_ID and SIMP_TYPE_RELIMAGE_ID in SIMP_RELIMAGE_ID.

16 December 2010

• curprev 14:4414:44, 16 December 2010‎ imported>Benoit‎ 31,413 bytes +246‎ Added rules SIMP_MULTI_DOMSUB_RAN and SIMP_MULTI_RANSUB_DOM.
• curprev 14:1614:16, 16 December 2010‎ imported>Benoit‎ 31,167 bytes +224‎ Added rules SIMP_RANRES_ID and SIMP_RANSUB_ID
• curprev 13:5113:51, 16 December 2010‎ imported>Benoit‎ 30,943 bytes +570‎ Added rules SIMP_DOMRES_DOMSUB_ID, SIMP_RANRES_DOMSUB_ID, SIMP_DOMSUB_DOMSUB_ID, SIMP_RANSUB_DOMSUB_ID.
• curprev 13:3513:35, 16 December 2010‎ imported>Benoit‎ m 30,373 bytes +28‎ Renamed SIMP_DOMRES_ID, SIMP_RANRES_ID, SIMP_DOMSUB_ID, SIMP_RANSUB_ID by adding the inner operator name : DOMRES

10 December 2010

• curprev 11:2711:27, 10 December 2010‎ imported>Benoit‎ m 30,345 bytes −22‎ Simplified the syntax of rule SIMP_MULTI_FUNIMAGE_OVERL_SETENUM
• curprev 10:3410:34, 10 December 2010‎ imported>Benoit‎ m 30,367 bytes −44‎ Simplified the syntax of rules SIMP_MULTI_FUNIMAGE_SETENUM_LR and SIMP_MULTI_FUNIMAGE_BUNION_SETENUM

9 December 2010

• curprev 16:0516:05, 9 December 2010‎ imported>Benoit‎ m 30,411 bytes 0‎ renamed SIMP_DOM_COMPSET and SIMP_RAN_COMPSET in SIMP_DOM_SETENUM and SIMP_RAN_SETENUM

7 December 2010

• curprev 17:0617:06, 7 December 2010‎ imported>Benoit‎ m 30,411 bytes 0‎ removed a semicolumn in SIMP_TYPE_OVERL_CPROD

6 December 2010

• curprev 19:2819:28, 6 December 2010‎ imported>Laurent‎ 30,411 bytes +26‎ Extended rule SIMP_TYPE_OVERL_CPROD.
• curprev 18:3818:38, 6 December 2010‎ imported>Laurent‎ 30,385 bytes −152‎ Removed SIMP_SPECIAL_LAMBDA (subsumed by SIMP_COMPSET_BFALSE) and generalized SIMP_DOM_LAMBDA and SIMP_RAN_LAMBDA.

3 December 2010

• curprev 13:2213:22, 3 December 2010‎ imported>Laurent‎ 30,537 bytes +347‎ Added rules SIMP_IN_FUNIMAGE*.

2 December 2010

• curprev 10:4310:43, 2 December 2010‎ imported>Benoit‎ m 30,190 bytes −1‎ No edit summary
• curprev 10:4210:42, 2 December 2010‎ imported>Benoit‎ 30,191 bytes −51‎ Replaced SIMP_TYPE_CONVERSE, SIMP_TYPE_DPROD, SIMP_TYPE_PPROD by SIMP_CONVERSE_CPROD, SIMP_DPROD_CPROD, SIMP_PPROD_CPROD which are more general. Rewrote SIMP_TYPE_OVERL_CPROD which was incorrect.
• curprev 10:1410:14, 2 December 2010‎ imported>Benoit‎ 30,242 bytes −305‎ No edit summary

23 November 2010

• curprev 12:0212:02, 23 November 2010‎ imported>Laurent‎ m 30,547 bytes +4‎ Fixed typo in SIMP_TYPE_DOM and SIMP_TYPE_RES (the condition did not typecheck)

22 November 2010

• curprev 13:2413:24, 22 November 2010‎ imported>Laurent‎ 30,543 bytes −356‎ Removed rules SIMP_SPECIAL_(ID|PRJ1|PRJ2) that were redundant.
• curprev 13:1913:19, 22 November 2010‎ imported>Laurent‎ 30,899 bytes +120‎ Undo revision 7532 by Laurent (Talk)
• curprev 13:0113:01, 22 November 2010‎ imported>Laurent‎ 30,779 bytes −120‎ Merged rules SIMP_TYPE_RELIMAGE_ID and SIMP_RELIMAGE_ID

16 November 2010

• curprev 14:4314:43, 16 November 2010‎ imported>Laurent‎ m 30,899 bytes 0‎ Marked rule SIMP_SPECIAL_RELIMAGE_L as implemented
• curprev 14:3814:38, 16 November 2010‎ imported>Laurent‎ m 30,899 bytes 0‎ Marked rules SIMP_SPECIAL_FCOMP and SIMP_SPECIAL_BCOMP as implemented
• curprev 13:5213:52, 16 November 2010‎ imported>Laurent‎ m 30,899 bytes +2‎ Marked rules SIMP_FUNIMAGE_LAMBDA and SIMP_FUNIMAGE_CONVERSE_FUNIMAGE as implemented

10 November 2010

• curprev 12:3212:32, 10 November 2010‎ imported>Laurent‎ m 30,897 bytes 0‎ No edit summary
• curprev 08:3208:32, 10 November 2010‎ imported>Laurent‎ 30,897 bytes 0‎ Marked rules prjone-functional and prjtwo-functional as broken (E and F can be arbitrary sets, not just types)

27 October 2010

• curprev 13:1613:16, 27 October 2010‎ imported>Laurent‎ 30,897 bytes +10‎ Proposed improvement to SIMP_TYPE_OVERL_CPROD

11 October 2010

• curprev 16:0916:09, 11 October 2010‎ imported>Desaperh‎ m 30,887 bytes 0‎ added rule DEF_IN_REL

30 September 2010

• curprev 15:2215:22, 30 September 2010‎ imported>Laurent‎ 30,887 bytes −41‎ Fixed rule DEF_IN_REL (replaced by the verbatim definition from Abrial's book).

29 September 2010

• curprev 15:3115:31, 29 September 2010‎ imported>Laurent‎ 30,928 bytes +156‎ Added rule DEF_IN_REL

17 September 2010

• curprev 13:3213:32, 17 September 2010‎ imported>Laurent‎ m 30,772 bytes +22‎ Fix of the fix
• curprev 13:3013:30, 17 September 2010‎ imported>Laurent‎ m 30,750 bytes +4‎ Fixed typos

30 August 2010

• curprev 12:1612:16, 30 August 2010‎ imported>Wohuai‎ m 30,746 bytes +309‎ No edit summary

26 August 2010

• curprev 16:1116:11, 26 August 2010‎ imported>Laurent‎ 30,437 bytes −216‎ Removed prjone-total (resp. prjtwo-total) which is subsumed by SIMP_DOM_PRJ1 (resp. SIMP_DOM_PRJ2).
• curprev 16:0616:06, 26 August 2010‎ imported>Laurent‎ 30,653 bytes −264‎ Removed duplicate rules