src/HOL/Enum.thy
changeset 54148 c8cc5ab4a863
parent 53015 a1119cf551e8
child 54295 45a5523d4a63
     1.1 --- a/src/HOL/Enum.thy	Fri Oct 18 10:43:20 2013 +0200
     1.2 +++ b/src/HOL/Enum.thy	Fri Oct 18 10:43:21 2013 +0200
     1.3 @@ -156,11 +156,11 @@
     1.4    "Id = image (\<lambda>x. (x, x)) (set Enum.enum)"
     1.5    by (auto intro: imageI in_enum)
     1.6  
     1.7 -lemma tranclp_unfold [code, no_atp]:
     1.8 +lemma tranclp_unfold [code]:
     1.9    "tranclp r a b \<longleftrightarrow> (a, b) \<in> trancl {(x, y). r x y}"
    1.10    by (simp add: trancl_def)
    1.11  
    1.12 -lemma rtranclp_rtrancl_eq [code, no_atp]:
    1.13 +lemma rtranclp_rtrancl_eq [code]:
    1.14    "rtranclp r x y \<longleftrightarrow> (x, y) \<in> rtrancl {(x, y). r x y}"
    1.15    by (simp add: rtrancl_def)
    1.16