Mercurial Mercurial > repos > isabelle / comparison
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Library/RBT.thy
changeset 45928 874845660119
parent 45694 4a8743618257
child 46133 d9fe85d3d2cd
equal deleted inserted replaced
45927:e0305e4f02c9 45928:874845660119 
   167 
   167 
   168 lemma distinct_keys [iff]:
 
   168 lemma distinct_keys [iff]:
 
   169   "distinct (keys t)"
 
   169   "distinct (keys t)"
 
   170   by (simp add: keys_def RBT_Impl.keys_def distinct_entries)
 
   170   by (simp add: keys_def RBT_Impl.keys_def distinct_entries)
 
   171 
   171 
       
   172 subsection {* Quickcheck generators *}
 
       
   173 
       
   174 quickcheck_generator rbt constructors: empty, insert
 
   172 
   175 
   173 end
 
   176 end
isabelle