Commit 21d98832 authored by paulson's avatar paulson
Browse files

merged

This diff is collapsed.
This diff is collapsed.
......@@ -789,6 +789,9 @@ proof -
using assms by (metis Ord_linear2 Sup_least Sup_upper eq_iff mem_Collect_eq subsetD succ_le_iff)
qed
lemma in_succ_iff: "Ord i \<Longrightarrow> j \<in> elts (ZFC_in_HOL.succ i) \<longleftrightarrow> Ord j \<and> j \<le> i"
by (metis Ord_in_Ord Ord_mem_iff_lt Ord_not_le Ord_succ succ_le_iff)
lemma zero_in_succ [simp,intro]: "Ord i \<Longrightarrow> 0 \<in> elts (succ i)"
using mem_0_Ord by auto
......
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