Commit f7c329b5 authored by nipkow's avatar nipkow


parent 0cbb56f4445a
......@@ -103,7 +103,7 @@ lemma del_left_size:
auto split: prod.splits)
lemma del_left_braun:
"del_left t = (x,t') \<Longrightarrow> braun t \<Longrightarrow> t \<noteq> Leaf \<Longrightarrow> braun t'"
"del_left t = (x,t') \<Longrightarrow> t \<noteq> Leaf \<Longrightarrow> braun t \<Longrightarrow> braun t'"
by(induction t arbitrary: x t' rule: del_left.induct;
auto split: prod.splits dest: del_left_size)
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