reverting 46c2c96f5d92 as it only provides mostly non-terminating executions for generated code
authorbulwahn
Sat Jan 28 06:13:03 2012 +0100 (2012-01-28)
changeset 46349b159ca4e268b
parent 46348 ee5009212793
child 46350 a49c89df7c92
reverting 46c2c96f5d92 as it only provides mostly non-terminating executions for generated code
src/HOL/Wellfounded.thy
     1.1 --- a/src/HOL/Wellfounded.thy	Fri Jan 27 19:08:48 2012 +0100
     1.2 +++ b/src/HOL/Wellfounded.thy	Sat Jan 28 06:13:03 2012 +0100
     1.3 @@ -615,13 +615,6 @@
     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