Removed sorry's.
This commit is contained in:
parent
f290da191d
commit
2f0da5f6ba
|
@ -609,8 +609,6 @@ lemma rule_charn2:
|
||||||
case Nil show ?case using Nil by simp
|
case Nil show ?case using Nil by simp
|
||||||
next
|
next
|
||||||
case (snoc y ys)
|
case (snoc y ys)
|
||||||
then have * : " y = AllowPortFromTo c d po \<Longrightarrow> ys \<noteq> []" sorry
|
|
||||||
have ** : "applied_rule_rev C x ys = Some (AllowPortFromTo c d po)" sledgehammer sorry
|
|
||||||
show ?case using snoc
|
show ?case using snoc
|
||||||
apply (case_tac "y = (AllowPortFromTo c d po)", simp_all )
|
apply (case_tac "y = (AllowPortFromTo c d po)", simp_all )
|
||||||
apply (simp add: applied_rule_rev_def)
|
apply (simp add: applied_rule_rev_def)
|
||||||
|
|
Loading…
Reference in New Issue