summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | haftmann |

Mon, 01 Mar 2021 08:16:22 +0100 | |

changeset 73576 | 2aef2de6b17c |

parent 73575 | ff24fe85ee57 |

child 73577 | 00e0f7724c06 |

child 73578 | 0fb889c361e6 |

NEWS

NEWS | file | annotate | diff | comparison | revisions | |

src/HOL/Library/List_Permutation.thy | file | annotate | diff | comparison | revisions |

--- a/NEWS Sun Feb 28 20:13:07 2021 +0000 +++ b/NEWS Mon Mar 01 08:16:22 2021 +0100 @@ -19,7 +19,11 @@ corrected. Minor INCOMPATIBILITY. * Theory "Permutation" in HOL-Library has been renamed to the more -specific "List_Permutation". +specific "List_Permutation". Note that most notions from that +theory are already present in theory "Permutations". INCOMPATIBILITY. + +* Lemma "permutes_induct" has been given named premised. +INCOMPATIBILITY. *** ML ***

--- a/src/HOL/Library/List_Permutation.thy Sun Feb 28 20:13:07 2021 +0000 +++ b/src/HOL/Library/List_Permutation.thy Mon Mar 01 08:16:22 2021 +0100 @@ -8,6 +8,12 @@ imports Permutations begin +text \<open> + Note that multisets already provide the notion of permutated list and hence + this theory mostly echoes material already logically present in theory + \<^text>\<open>Permutations\<close>; it should be seldom needed. +\<close> + subsection \<open>An inductive definition \ldots\<close> inductive perm :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool" (infixr \<open><~~>\<close> 50)