src/HOL/Wfrec.thy

--- a/src/HOL/Wfrec.thy	Tue Nov 09 11:23:27 2021 +0100
+++ b/src/HOL/Wfrec.thy	Tue Nov 09 16:04:11 2021 +0000
@@ -84,6 +84,9 @@
   finally show "wfrec R F x = F (wfrec R F) x" .
 qed
 
+lemma wfrec_def_adm: "f \<equiv> wfrec R F \<Longrightarrow> wf R \<Longrightarrow> adm_wf R F \<Longrightarrow> f = F f"
+  using wfrec_fixpoint by simp
+
 
 subsection \<open>Wellfoundedness of \<open>same_fst\<close>\<close>