equal
deleted
inserted
replaced
91 "(\<forall>y. (y,x) \<in> r \<longrightarrow> y \<in> acc r) \<Longrightarrow> x \<in> acc r" |
91 "(\<forall>y. (y,x) \<in> r \<longrightarrow> y \<in> acc r) \<Longrightarrow> x \<in> acc r" |
92 |
92 |
93 lemma "wf{(x,y). (x,y) \<in> r \<and> y \<in> acc r}" |
93 lemma "wf{(x,y). (x,y) \<in> r \<and> y \<in> acc r}" |
94 thm wfI |
94 thm wfI |
95 apply(rule_tac A = "acc r" in wfI) |
95 apply(rule_tac A = "acc r" in wfI) |
96 apply (blast elim:acc.elims) |
96 apply (blast elim: acc.elims) |
97 apply(simp(no_asm_use)) |
97 apply(simp(no_asm_use)) |
98 thm acc.induct |
98 thm acc.induct |
99 apply(erule acc.induct) |
99 apply(erule acc.induct) |
100 by blast |
100 by blast |
101 |
101 |