src/HOL/Wellfounded.thy
changeset 46333 46c2c96f5d92
parent 46177 adac34829e10
child 46349 b159ca4e268b
equal deleted inserted replaced
46332:f62f5f1fda3b 46333:46c2c96f5d92
   613 
   613 
   614 lemmas acc_subset = accp_subset [to_set]
   614 lemmas acc_subset = accp_subset [to_set]
   615 
   615 
   616 lemmas acc_subset_induct = accp_subset_induct [to_set]
   616 lemmas acc_subset_induct = accp_subset_induct [to_set]
   617 
   617 
       
   618 text {* Very basic code generation setup *}
       
   619 
       
   620 declare accp.simps[code]
       
   621 
       
   622 lemma [code_unfold]:
       
   623   "(x : acc r) = accp (%x xa. (x, xa) : r) x"
       
   624 by (simp add: accp_acc_eq)
   618 
   625 
   619 subsection {* Tools for building wellfounded relations *}
   626 subsection {* Tools for building wellfounded relations *}
   620 
   627 
   621 text {* Inverse Image *}
   628 text {* Inverse Image *}
   622 
   629