--- a/src/HOL/BNF_Def.thy Mon Mar 16 23:00:38 2015 +0100
+++ b/src/HOL/BNF_Def.thy Mon Mar 16 23:05:56 2015 +0100
@@ -228,6 +228,12 @@
lemma comp_apply_eq: "f (g x) = h (k x) \<Longrightarrow> (f \<circ> g) x = (h \<circ> k) x"
unfolding comp_apply by assumption
+lemma refl_ge_eq: "(\<And>x. R x x) \<Longrightarrow> op = \<le> R"
+ by auto
+
+lemma ge_eq_refl: "op = \<le> R \<Longrightarrow> R x x"
+ by auto
+
ML_file "Tools/BNF/bnf_util.ML"
ML_file "Tools/BNF/bnf_tactics.ML"
ML_file "Tools/BNF/bnf_def_tactics.ML"