src/HOL/Wellfounded.thy
changeset 54295 45a5523d4a63
parent 49945 fb696ff1f086
child 55027 a74ea6d75571
     1.1 --- a/src/HOL/Wellfounded.thy	Sun Nov 10 10:02:34 2013 +0100
     1.2 +++ b/src/HOL/Wellfounded.thy	Sun Nov 10 15:05:06 2013 +0100
     1.3 @@ -482,6 +482,11 @@
     1.4  
     1.5  lemmas accpI = accp.accI
     1.6  
     1.7 +lemma accp_eq_acc [code]:
     1.8 +  "accp r = (\<lambda>x. x \<in> Wellfounded.acc {(x, y). r x y})"
     1.9 +  by (simp add: acc_def)
    1.10 +
    1.11 +
    1.12  text {* Induction rules *}
    1.13  
    1.14  theorem accp_induct:
    1.15 @@ -855,4 +860,7 @@
    1.16  
    1.17  declare "prod.size" [no_atp]
    1.18  
    1.19 +
    1.20 +hide_const (open) acc accp
    1.21 +
    1.22  end