Inference Rules: Revision history

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

8 July 2009

• curprev 10:2510:25, 8 July 2009‎ imported>Laurent‎ m 17,973 bytes −756‎ Fixed rule names to make them easy to extract
• curprev 09:3609:36, 8 July 2009‎ imported>Laurent‎ 18,729 bytes +259‎ Added AUTO_MH

6 July 2009

• curprev 13:2813:28, 6 July 2009‎ imported>Laurent‎ m 18,470 bytes +18‎ No edit summary
• curprev 13:2113:21, 6 July 2009‎ imported>Laurent‎ m 18,452 bytes +1‎ Renamed SIM_FUN into FUN_GOAL.
• curprev 13:1813:18, 6 July 2009‎ imported>Laurent‎ m 18,451 bytes −5‎ No edit summary
• curprev 13:1813:18, 6 July 2009‎ imported>Laurent‎ 18,456 bytes +386‎ Added SIM_FUN
• curprev 10:1510:15, 6 July 2009‎ imported>Laurent‎ m 18,070 bytes −15‎ Fixed DIS_SETMINUS_R

3 July 2009

• curprev 14:4814:48, 3 July 2009‎ imported>Nicolas‎ m 18,085 bytes +386‎ added DISTINCT_CASE
• curprev 14:2614:26, 3 July 2009‎ imported>Nicolas‎ m 17,699 bytes +304‎ added EXISTS_INST
• curprev 14:2214:22, 3 July 2009‎ imported>Nicolas‎ m 17,395 bytes +30‎ added H as hyposthesis for WD in FORALL_INST, FORALL_INST_MP, CUT
• curprev 14:2014:20, 3 July 2009‎ imported>Nicolas‎ m 17,365 bytes −37‎ removed bold font in WD ;; used correct symbol for :=
• curprev 14:0914:09, 3 July 2009‎ imported>Nicolas‎ m 17,402 bytes +359‎ added CUT
• curprev 13:5013:50, 3 July 2009‎ imported>Nicolas‎ m 17,043 bytes +482‎ added FORALL_INST_MP
• curprev 13:3813:38, 3 July 2009‎ imported>Nicolas‎ m 16,561 bytes +247‎ added FORALL_INST