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