Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
clarified heading
authorhaftmann
Thu, 12 May 2016 14:38:53 +0200
changeset 63089 40134ddec3bf
parent 63088 f2177f5d2aed
child 63090 7aa9ac5165e4
clarified heading
src/HOL/Library/Multiset.thy file | annotate | diff | comparison | revisions 
--- a/src/HOL/Library/Multiset.thy	Thu May 12 09:34:07 2016 +0200
+++ b/src/HOL/Library/Multiset.thy	Thu May 12 14:38:53 2016 +0200
@@ -2066,7 +2066,7 @@
     \<Longrightarrow> (I + K, I + J) \<in> mult r"
 using one_step_implies_mult_aux by blast
 
-subsection \<open>A quasi-recursive characterization\<close>
+subsection \<open>A quasi-executable characterization\<close>
 
 text \<open>
   The decreasing parts \<open>A\<close> and \<open>B\<close> of multisets in a multiset-comparison
isabelle