adbrucker
/
lh-l4v
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

lib: rename lemma to prevent collision with List.sorted_filter

This commit is contained in:
IlmariReissumies 2019-04-05 12:12:49 +11:00
parent 7637422a10
commit 0eefa4b6b6
1 changed files with 1 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
lib/LemmaBucket.thy
View File

@ -478,7 +478,7 @@ lemma foldl_fun_or_alt:
apply clarsimp
by (simp add: foldl_map)
lemma sorted_filter:
lemma sorted_imp_sorted_filter:
"sorted xs \<Longrightarrow> sorted (filter P xs)"
by (metis filter_sort sorted_sort sorted_sort_id)