--- a/src/HOL/Wfrec.thy Thu Jan 16 15:47:33 2014 +0100
+++ b/src/HOL/Wfrec.thy Thu Jan 16 16:20:17 2014 +0100
@@ -7,7 +7,7 @@
header {* Well-Founded Recursion Combinator *}
theory Wfrec
-imports Main
+imports Wellfounded
begin
inductive
@@ -74,26 +74,6 @@
done
-subsection {* Nitpick setup *}
-
-axiomatization wf_wfrec :: "('a \<times> 'a) set \<Rightarrow> (('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b"
-
-definition wf_wfrec' :: "('a \<times> 'a) set \<Rightarrow> (('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b" where
-[nitpick_simp]: "wf_wfrec' R F x = F (cut (wf_wfrec R F) R x) x"
-
-definition wfrec' :: "('a \<times> 'a) set \<Rightarrow> (('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b" where
-"wfrec' R F x \<equiv> if wf R then wf_wfrec' R F x
- else THE y. wfrec_rel R (%f x. F (cut f R x) x) x y"
-
-setup {*
- Nitpick_HOL.register_ersatz_global
- [(@{const_name wf_wfrec}, @{const_name wf_wfrec'}),
- (@{const_name wfrec}, @{const_name wfrec'})]
-*}
-
-hide_const (open) wf_wfrec wf_wfrec' wfrec'
-hide_fact (open) wf_wfrec'_def wfrec'_def
-
subsection {* Wellfoundedness of @{text same_fst} *}
definition