summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
file |
latest |
revisions |
annotate |
diff |
comparison |
raw |
help

NEWS

changeset 73878 | 4dc3baf45d6a |

parent 73872 | b0ea03e837b1 |

child 73879 | 5020054b3a16 |

equal
deleted
inserted
replaced

73877:b4b70d13c995 | 73878:4dc3baf45d6a |
---|---|

81 INCOMPATIBILITY; note that for most applications less elementary lemmas |
81 INCOMPATIBILITY; note that for most applications less elementary lemmas |

82 exists. |
82 exists. |

83 |
83 |

84 * Dedicated session HOL-Combinatorics. INCOMPATIBILITY: theories |
84 * Dedicated session HOL-Combinatorics. INCOMPATIBILITY: theories |

85 "Permutations", "List_Permutation" (formerly "Permutation"), "Stirling", |
85 "Permutations", "List_Permutation" (formerly "Permutation"), "Stirling", |

86 "Multiset_Permutations" have been |
86 "Multiset_Permutations", "Perm" have been moved there from session |

87 moved there from session HOL-Library. See theory "Guide" for an |
87 HOL-Library. See theory "Guide" for an overview about existing material |

88 overview about existing material on basic combinatorics. |
88 on basic combinatorics. |

89 |
89 |

90 * Theory "Permutation" in HOL-Library has been renamed to the more |
90 * Theory "Permutation" in HOL-Library has been renamed to the more |

91 specific "List_Permutation". Note that most notions from that |
91 specific "List_Permutation". Note that most notions from that |

92 theory are already present in theory "Permutations". INCOMPATIBILITY. |
92 theory are already present in theory "Permutations". INCOMPATIBILITY. |

93 |
93 |