crefine: Remove a find_theorems invocation.
This commit is contained in:
parent
7bc4236077
commit
d9154d00af
|
@ -790,8 +790,6 @@ lemma list_map_length_is_None [simp]:
|
||||||
apply (simp add: list_map_def)
|
apply (simp add: list_map_def)
|
||||||
done
|
done
|
||||||
|
|
||||||
find_theorems h_t_valid intvl
|
|
||||||
|
|
||||||
lemma list_map_append_one:
|
lemma list_map_append_one:
|
||||||
"list_map (xs @ [x]) = [length xs \<mapsto> x] ++ list_map xs"
|
"list_map (xs @ [x]) = [length xs \<mapsto> x] ++ list_map xs"
|
||||||
by (simp add: list_map_def)
|
by (simp add: list_map_def)
|
||||||
|
|
Loading…
Reference in New Issue