theory Simproc_Match_Not_Working
imports Main
begin

ML\<open>
fun sum_prod_simproc _ _ _ = 
let
  val _ = Pretty.writeln (Pretty.str "simproc triggered")
in
  NONE
end
\<close>

simproc_setup sum_prod ("prod f A" | "sum f B") = \<open>sum_prod_simproc\<close>

lemma "(\<Sum>i=1..3. i) = (\<Sum>i=0..2. i + 1)"
  apply simp
  sorry

lemma "(\<Prod>i=1..3. i) = (\<Prod>i=0..2. i + 1)"
  apply simp
  sorry



end