Commit 44b954be authored by Alexander Bentkamp's avatar Alexander Bentkamp
Browse files

Remove old todo

--HG--
branch : deep_learning
parent d17090cd59d8
......@@ -239,8 +239,6 @@ proof -
by metis
then show ?thesis unfolding lookup_tensors_from_net[OF 1 2 3]
using polyfun_evaluate_net[OF base_input_length[OF 2, unfolded input_sizes, symmetric] assms(1) assms(3), of s]
(* TODO: Investigate why sledgehammer fails:
using polyfun_evaluate_net[OF base_input_length[OF 2, unfolded input_sizes, symmetric] assms(1) assms(3)] sledgehammer *)
by simp
qed
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment