--- a/src/HOL/Partial_Function.thy Wed Feb 11 13:58:51 2015 +0100
+++ b/src/HOL/Partial_Function.thy Wed Feb 11 14:03:05 2015 +0100
@@ -236,6 +236,15 @@
qed
qed (auto simp: flat_ord_def)
+lemma flat_ordI: "(x \<noteq> a \<Longrightarrow> x = y) \<Longrightarrow> flat_ord a x y"
+by(auto simp add: flat_ord_def)
+
+lemma flat_ord_antisym: "\<lbrakk> flat_ord a x y; flat_ord a y x \<rbrakk> \<Longrightarrow> x = y"
+by(auto simp add: flat_ord_def)
+
+lemma antisymP_flat_ord: "antisymP (flat_ord a)"
+by(rule antisymI)(auto dest: flat_ord_antisym)
+
interpretation tailrec!:
partial_function_definitions "flat_ord undefined" "flat_lub undefined"
where "flat_lub undefined {} \<equiv> undefined"