Set Rewrite Rules: Revision history

13 April 2023

• curprev 14:3314:33, 13 April 2023‎ Guillaume talk contribs‎ 29,892 bytes 0‎ Rules SIMP_{EMPTY,SINGLE}_PARTITION were implemented

6 April 2023

• curprev 09:3109:31, 6 April 2023‎ Guillaume talk contribs‎ 29,892 bytes 0‎ Rules DEF_EQUAL_CARD and SIMP_EQUAL_CARD are implemented as of Rodin 3.8

25 November 2022

• curprev 15:1815:18, 25 November 2022‎ Guillaume talk contribs‎ 29,892 bytes +350‎ Add rules for cardinal equality

21 October 2022

• curprev 15:3015:30, 21 October 2022‎ Guillaume talk contribs‎ 29,542 bytes −2‎ Move rewrite rules for KUNION and QUNION to the commented-out section for disabled rules, as they are false

17 October 2022

• curprev 09:2609:26, 17 October 2022‎ Guillaume talk contribs‎ 29,544 bytes +133‎ add note about finiteness of infinite union

2 October 2013

• curprev 17:1617:16, 2 October 2013‎ imported>Laurent‎ 29,411 bytes +254‎ Add rules SIMP_EMPTY_PARTITION and SIMP_SINGLE_PARTITION

2 May 2013

• curprev 15:1915:19, 2 May 2013‎ imported>Josselin‎ 29,157 bytes −172‎ Removed SIMP_TYPE_EQUAL_EMPTY (moved to Empty Set Rewrite Rules)
• curprev 15:1715:17, 2 May 2013‎ imported>Josselin‎ 29,329 bytes −166‎ Removed SIMP_SPECIAL_EQUAL_COMPSET (moved to Empty Set Rewrite Rules)
• curprev 15:1415:14, 2 May 2013‎ imported>Josselin‎ 29,495 bytes −188‎ Removed DEF_SPECIAL_NOT_EQUAL (moved to Empty Set Rewrite Rules)

29 September 2011

• curprev 14:5114:51, 29 September 2011‎ imported>Billaude‎ 29,683 bytes +1‎ DEF_IN_MAPSTO rule is now automatic with the AutoRewriterL3.

28 September 2011

• curprev 13:3113:31, 28 September 2011‎ imported>Laurent‎ 29,682 bytes 0‎ Marked some rules as implemented

19 September 2011

• curprev 07:0207:02, 19 September 2011‎ imported>Laurent‎ m 29,682 bytes +1‎ Renamed rule SIMP_MULTI_IMP_OR into SIMP_MULTI_IMP_AND

8 July 2011

• curprev 20:5220:52, 8 July 2011‎ imported>Laurent‎ 29,681 bytes +143‎ Added rule SIMP_EXISTS_IMP
• curprev 18:0118:01, 8 July 2011‎ imported>Laurent‎ 29,538 bytes +204‎ Added rules SIMP_MULTI_IMP_NOT_*

28 January 2011

• curprev 14:3114:31, 28 January 2011‎ imported>Tommy‎ m 29,334 bytes +1‎ Since r10735, the rule SIMP_NOT_NOT is both manual and automatic. The manual part of the rule is implemented in the remove negation tactic.

26 January 2011

• curprev 16:5616:56, 26 January 2011‎ imported>Laurent‎ 29,333 bytes −1‎ Typo.
• curprev 16:2716:27, 26 January 2011‎ imported>Benoit‎ m 29,334 bytes −3‎ Correction on rule SIMP_SPECIAL_COMPSET_BTRUE
• curprev 16:2516:25, 26 January 2011‎ imported>Benoit‎ 29,337 bytes −39‎ Updated rules SIMP_SPECIAL_COMPSET_BTRUE, SIMP_COMPSET_EQUAL, and added a star to DEF_FINITE.
• curprev 10:0710:07, 26 January 2011‎ imported>Benoit‎ 29,376 bytes +218‎ Added rule SIMP_COMPSET

25 January 2011

• curprev 13:5013:50, 25 January 2011‎ imported>Benoit‎ m 29,158 bytes −14‎ Simplified rule DEF_FINITE

19 January 2011

• curprev 13:2013:20, 19 January 2011‎ imported>Benoit‎ 29,172 bytes 0‎ Marked DERIV_SUBSETEQ_BUNION and DERIV_SUBSETEQ_BINTER as automatic.

18 January 2011

• curprev 17:1417:14, 18 January 2011‎ imported>Laurent‎ 29,172 bytes +1‎ Improved rule SIMP_COMPSET_EQUAL.
• curprev 16:3316:33, 18 January 2011‎ imported>Laurent‎ 29,171 bytes 0‎ Marked rule SIMP_SUBSETEQ_COMPSET_R as manual.
• curprev 09:0809:08, 18 January 2011‎ imported>Benoit‎ 29,171 bytes −505‎ Removed rules SIMP_SPECIAL_FORALL_BTRUE, SIMP_SPECIAL_FORALL_BFALSE, SIMP_SPECIAL_EXISTS_BTRUE, SIMP_SPECIAL_EXISTS_BFALSE.
• curprev 09:0509:05, 18 January 2011‎ imported>Benoit‎ 29,676 bytes +107‎ Added rule SIMP_FINITE_BOOL.

17 January 2011

• curprev 17:3017:30, 17 January 2011‎ imported>Benoit‎ m 29,569 bytes +1‎ Added stars to the automatic rules implemented in auto rewriter L2.
• curprev 17:1517:15, 17 January 2011‎ imported>Benoit‎ m 29,568 bytes +4‎ Added stars to the automatic rules implemented in auto rewriter L2.
• curprev 17:1017:10, 17 January 2011‎ imported>Benoit‎ m 29,564 bytes +5‎ Added stars to the automatic rules implemented in auto rewriter L2.
• curprev 16:4916:49, 17 January 2011‎ imported>Benoit‎ m 29,559 bytes +14‎ Added stars to the automatic rules implemented in auto rewriter L2.

14 January 2011

• curprev 15:0415:04, 14 January 2011‎ imported>Benoit‎ 29,545 bytes +185‎ Added rule SIMP_COMPSET_SUBSETEQ.

13 January 2011

• curprev 09:3509:35, 13 January 2011‎ imported>Laurent‎ 29,360 bytes −3‎ Normalised rule SIMP_SPECIAL_SUBSET_L.

15 December 2010

• curprev 16:4316:43, 15 December 2010‎ imported>Laurent‎ 29,363 bytes −382‎ Removed subsumed rules SIMP_TYPE_KUNION and SIMP_TYPE_KINTER.

8 December 2010

• curprev 13:5513:55, 8 December 2010‎ imported>Benoit‎ 29,745 bytes +652‎ Added rules SIMP_FINITE_PRJ1, SIMP_FINITE_PRJ2, SIMP_FINITE_PRJ1_DOMRES and SIMP_FINITE_PRJ2_DOMRES
• curprev 13:3513:35, 8 December 2010‎ imported>Benoit‎ 29,093 bytes +124‎ added rule SIMP_FINITE_ID_DOMRES

6 December 2010

• curprev 19:1919:19, 6 December 2010‎ imported>Laurent‎ 28,969 bytes +284‎ Added missing side condition to SIMP_FINITE_LAMBDA.
• curprev 18:3318:33, 6 December 2010‎ imported>Laurent‎ 28,685 bytes −6‎ Generalized rule SIMP_FINITE_LAMBDA

3 December 2010

• curprev 14:4914:49, 3 December 2010‎ imported>Laurent‎ 28,691 bytes +181‎ Added rules SIMP_FINITE_UNION and SIMP_FINITE_QUNION

2 December 2010

• curprev 10:1910:19, 2 December 2010‎ imported>Benoit‎ 28,510 bytes −195‎ No edit summary

10 November 2010

• curprev 12:3212:32, 10 November 2010‎ imported>Laurent‎ m 28,705 bytes −1‎ No edit summary
• curprev 08:4908:49, 10 November 2010‎ imported>Laurent‎ m 28,706 bytes +866‎ No edit summary

27 October 2010

• curprev 13:1313:13, 27 October 2010‎ imported>Laurent‎ 27,840 bytes −370‎ Removed rules about overriding which belong to set rewrite.
• curprev 13:0913:09, 27 October 2010‎ imported>Laurent‎ 28,210 bytes −506‎ Removed rules SIMP_SPECIAL_FORALL_BTRUE, SIMP_SPECIAL_FORALL_BFALSE, SIMP_SPECIAL_EXISTS_BTRUE, and SIMP_SPECIAL_EXISTS_BFALSE which are subsumed by SIMP_FORALL and SIMP_EXISTS respectively.
• curprev 13:0113:01, 27 October 2010‎ imported>Laurent‎ 28,716 bytes +10‎ Proposed improvement to SIMP_TYPE_OVERL_CPROD
• curprev 12:5112:51, 27 October 2010‎ imported>Laurent‎ 28,706 bytes 0‎ Proposed improvement to SIMP_SPECIAL_COMPSET_BFALSE
• curprev 12:2612:26, 27 October 2010‎ imported>Laurent‎ 28,706 bytes +112‎ Added rule SIMP_KINTER_POW (needs checking)
• curprev 10:2410:24, 27 October 2010‎ imported>Laurent‎ 28,594 bytes +2‎ Marked rules SIMP_FORALL and SIMP_EXISTS as implemented
• curprev 09:4609:46, 27 October 2010‎ imported>Laurent‎ 28,592 bytes −123‎ Removed rule SIMP_MULTI_EQV_NOT_NOT which is subsumed by SIMP_MULTI_EQV.
• curprev 09:4209:42, 27 October 2010‎ imported>Laurent‎ m 28,715 bytes +4‎ Marked rules SIMP_MULTI_AND, SIMP_MULTI_AND_NOT, SIMP_MULTI_OR, and SIMP_MULTI_OR_NOT as implemented

17 September 2010

• curprev 13:2313:23, 17 September 2010‎ imported>Laurent‎ m 28,711 bytes 0‎ Fixed typo

30 August 2010

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