src/HOL/Library/Predicate_Compile_Alternative_Defs.thy
changeset 56679 5545bfdfefcc
parent 56073 29e308b56d23
child 60045 cd2b6debac18
     1.1 --- a/src/HOL/Library/Predicate_Compile_Alternative_Defs.thy	Thu Apr 24 00:08:48 2014 +0200
     1.2 +++ b/src/HOL/Library/Predicate_Compile_Alternative_Defs.thy	Thu Apr 24 00:23:38 2014 +0200
     1.3 @@ -174,16 +174,16 @@
     1.4  
     1.5  subsection {* Alternative rules for @{text length} *}
     1.6  
     1.7 -definition size_list :: "'a list => nat"
     1.8 -where "size_list = size"
     1.9 +definition size_list' :: "'a list => nat"
    1.10 +where "size_list' = size"
    1.11  
    1.12 -lemma size_list_simps:
    1.13 -  "size_list [] = 0"
    1.14 -  "size_list (x # xs) = Suc (size_list xs)"
    1.15 -by (auto simp add: size_list_def)
    1.16 +lemma size_list'_simps:
    1.17 +  "size_list' [] = 0"
    1.18 +  "size_list' (x # xs) = Suc (size_list' xs)"
    1.19 +by (auto simp add: size_list'_def)
    1.20  
    1.21 -declare size_list_simps[code_pred_def]
    1.22 -declare size_list_def[symmetric, code_pred_inline]
    1.23 +declare size_list'_simps[code_pred_def]
    1.24 +declare size_list'_def[symmetric, code_pred_inline]
    1.25  
    1.26  
    1.27  subsection {* Alternative rules for @{text list_all2} *}