Inference Rules: Revision history

14 December 2010

• curprev 12:5512:55, 14 December 2010‎ imported>Laurent‎ 24,570 bytes +237‎ Fixed FIN_QINTER_R and added FIN_KINTER_R

13 December 2010

• curprev 17:0417:04, 13 December 2010‎ imported>Nicolas‎ 24,333 bytes +195‎ added rule FIN_QINTER_R

16 November 2010

• curprev 13:4713:47, 16 November 2010‎ imported>Laurent‎ m 24,138 bytes 0‎ Marked rules ONE_POINT_L and ONE_POINT_R as implemented
• curprev 13:3413:34, 16 November 2010‎ imported>Laurent‎ m 24,138 bytes 0‎ Marked rule FUN_IMAGE_GOAL as implemented

15 October 2010

• curprev 08:2608:26, 15 October 2010‎ imported>Desaperh‎ 24,138 bytes 0‎ No edit summary

8 October 2010

• curprev 14:5614:56, 8 October 2010‎ imported>Desaperh‎ 24,138 bytes 0‎ Rule FUN_IMAGE_GOAL has been implemented

17 September 2010

• curprev 16:4716:47, 17 September 2010‎ imported>Laurent‎ 24,138 bytes −172‎ Removed WD-strictness condition where it was unnecessary and unimplemented.
• curprev 14:3214:32, 17 September 2010‎ imported>Laurent‎ 24,310 bytes −321‎ Replaced "top-level" with WD strictness or freeness condition.

9 September 2010

• curprev 12:2712:27, 9 September 2010‎ imported>Nicolas‎ m 24,631 bytes −1,120‎ moved datatype rules to extension proof rules page

6 September 2010

• curprev 08:5408:54, 6 September 2010‎ imported>Nicolas‎ m 25,751 bytes +34‎ added a link to datatype rule examples
• curprev 08:2508:25, 6 September 2010‎ imported>Nicolas‎ m 25,717 bytes −71‎ simplified representation of rule DATATYPE_INDUCTION (the meaning remains the same)

30 August 2010

• curprev 12:1412:14, 30 August 2010‎ imported>Wohuai‎ m 25,788 bytes +191‎ No edit summary

27 August 2010

• curprev 14:0814:08, 27 August 2010‎ imported>Laurent‎ 25,597 bytes 0‎ Rule FUN_IMAGE_GOAL is manual
• curprev 13:1313:13, 27 August 2010‎ imported>Laurent‎ 25,597 bytes +348‎ Added rule FUN_IMAGE_GOAL

25 August 2010

• curprev 16:5616:56, 25 August 2010‎ imported>Laurent‎ 25,249 bytes −238‎ Changed REC_FUN_GOAL to FUN_GOAL_REC and fixed typing.

23 August 2010

• curprev 13:1413:14, 23 August 2010‎ imported>Desaperh‎ 25,487 bytes +760‎ Added rule REC_FUN_GOAL
• curprev 13:1213:12, 23 August 2010‎ imported>Desaperh‎ 24,727 bytes −760‎ Undo revision 6711 by Desaperh (Talk)
• curprev 13:0913:09, 23 August 2010‎ imported>Desaperh‎ 25,487 bytes +760‎ No edit summary

6 August 2010

• curprev 13:5513:55, 6 August 2010‎ imported>Nicolas‎ 24,727 bytes +584‎ added DATATYPE_INDUCTION; rewrote DATATYPE_DISTINCT_CASE
• curprev 12:3812:38, 6 August 2010‎ imported>Nicolas‎ 24,143 bytes +625‎ added DATATYPE_DISTINCT_CASE

4 August 2010

• curprev 16:3716:37, 4 August 2010‎ imported>Pascal‎ 23,518 bytes +129‎ No edit summary

28 April 2010

• curprev 13:4713:47, 28 April 2010‎ imported>Tommy‎ 23,389 bytes −884‎ Rules OV_SETENUM_L (resp. OV_SETENUM_R) and OV_L (resp. OV_R) have been implemented in r8699.

21 April 2010

• curprev 16:4616:46, 21 April 2010‎ imported>Tommy‎ 24,273 bytes +13‎ Added rules FUNIMG_SET_DOMSUB_L and FUNIMG_DOMSUB_L
• curprev 16:3216:32, 21 April 2010‎ imported>Tommy‎ m 24,260 bytes +871‎ No edit summary
• curprev 15:2715:27, 21 April 2010‎ imported>Laurent‎ 23,389 bytes +6‎ Fixed rules OV_L, OV_R, OV_SETENUM_L, and OV_SETENUM_R.
• curprev 15:2015:20, 21 April 2010‎ imported>Tommy‎ m 23,383 bytes +80‎ No edit summary
• curprev 13:0613:06, 21 April 2010‎ imported>Tommy‎ m 23,303 bytes 0‎ No edit summary

27 March 2010

• curprev 22:3022:30, 27 March 2010‎ imported>Laurent‎ m 23,303 bytes +8‎ No edit summary

1 February 2010

• curprev 11:5611:56, 1 February 2010‎ imported>Laurent‎ 23,295 bytes +1,470‎ Added rules SIMP_CARD_SETMINUS_L, SIMP_CARD_SETMINUS_R, SIMP_CARD_CPROD_L and SIMP_CARD_CPROD_R (were previously rewrite rules).

15 January 2010

• curprev 11:0711:07, 15 January 2010‎ imported>Laurent‎ 21,825 bytes 0‎ Marked CARD_EMPTY_INTERV as not implemented.
• curprev 09:5009:50, 15 January 2010‎ imported>Laurent‎ 21,825 bytes 0‎ Implementation of rule EXISTS_INST has been confirmed correct

13 January 2010

• curprev 15:4315:43, 13 January 2010‎ imported>Tommy‎ m 21,825 bytes 0‎ Mark FIN_FUN_* as fixed(*). Fixed in r8042.

7 January 2010

• curprev 11:0811:08, 7 January 2010‎ imported>Laurent‎ 21,825 bytes +813‎ Replaced CARD_SUBSETEQ by DERIV_LE_CARD, DERIV_GE_CARD, DERIV_LT_CARD, DERIV_GT_CARD, DERIV_EQUAL_CARD.

23 December 2009

• curprev 11:5311:53, 23 December 2009‎ imported>Laurent‎ 21,012 bytes 0‎ Code for rules FIN_SUBSETEQ_R and FIN_REL_R is now fixed in Subversion.

21 December 2009

• curprev 09:2509:25, 21 December 2009‎ imported>Tommy‎ m 21,012 bytes −3‎ removed * on unimplemented rules

14 November 2009

• curprev 14:4714:47, 14 November 2009‎ imported>Laurent‎ m 21,015 bytes 0‎ Rules MH and HM have been fixed

11 November 2009

• curprev 18:0118:01, 11 November 2009‎ imported>Laurent‎ 21,015 bytes −32‎ Fixed EXISTS_INST which was on the wrong side.
• curprev 17:5617:56, 11 November 2009‎ imported>Laurent‎ m 21,047 bytes −354‎ Fixed silly side conditions
• curprev 17:4617:46, 11 November 2009‎ imported>Laurent‎ m 21,401 bytes −32‎ Fixed more spacing in formulas
• curprev 17:4017:40, 11 November 2009‎ imported>Laurent‎ m 21,433 bytes −293‎ FIxed spacing in formulas
• curprev 11:0711:07, 11 November 2009‎ imported>Laurent‎ 21,726 bytes +535‎ Fixed broken rules (ill-defined, ill-typed or plain wrong)

8 October 2009

• curprev 16:0816:08, 8 October 2009‎ imported>Nicolas‎ m 21,191 bytes −24‎ Undo revision 4260 by Nicolas (Talk)
• curprev 13:1813:18, 8 October 2009‎ imported>Nicolas‎ m 21,215 bytes +24‎ corrected FORALL_INST_MP: added [x:=E] P hypothesis to 3rd antecedent (similar to MH)

18 August 2009

• curprev 09:0409:04, 18 August 2009‎ imported>Nicolas‎ m 21,191 bytes +288‎ added SIM_REL_IMAGE_L (for implementation traceability purposes)
• curprev 08:5808:58, 18 August 2009‎ imported>Nicolas‎ m 20,903 bytes +301‎ added SIM_FCOMP_L (for implementation traceability purposes)
• curprev 08:5408:54, 18 August 2009‎ imported>Nicolas‎ m 20,602 bytes +369‎ added DIS_SETMINUS_L (for implementation traceability purposes)

17 August 2009

• curprev 14:0514:05, 17 August 2009‎ imported>Nicolas‎ m 20,233 bytes +840‎ added FIN_L_* rules
• curprev 13:2013:20, 17 August 2009‎ imported>Nicolas‎ m 19,393 bytes +362‎ added DIS_BINTER_L

15 July 2009

• curprev 09:0009:00, 15 July 2009‎ imported>Nicolas‎ m 19,031 bytes +172‎ Added comment for one point rule with 'exists' quantifier

10 July 2009

• curprev 14:5214:52, 10 July 2009‎ imported>Nicolas‎ m 18,859 bytes +886‎ added ONE_POINT_L