| changeset 46333 | 46c2c96f5d92 |
| parent 46177 | adac34829e10 |
| child 46349 | b159ca4e268b |
--- a/src/HOL/Wellfounded.thy Wed Jan 25 16:07:41 2012 +0100 +++ b/src/HOL/Wellfounded.thy Wed Jan 25 16:07:48 2012 +0100 @@ -615,6 +615,13 @@ lemmas acc_subset_induct = accp_subset_induct [to_set] +text {* Very basic code generation setup *} + +declare accp.simps[code] + +lemma [code_unfold]: + "(x : acc r) = accp (%x xa. (x, xa) : r) x" +by (simp add: accp_acc_eq) subsection {* Tools for building wellfounded relations *}