--- a/src/HOL/Library/Predicate_Compile_Alternative_Defs.thy Thu Apr 24 00:08:48 2014 +0200
+++ b/src/HOL/Library/Predicate_Compile_Alternative_Defs.thy Thu Apr 24 00:23:38 2014 +0200
@@ -174,16 +174,16 @@
subsection {* Alternative rules for @{text length} *}
-definition size_list :: "'a list => nat"
-where "size_list = size"
+definition size_list' :: "'a list => nat"
+where "size_list' = size"
-lemma size_list_simps:
- "size_list [] = 0"
- "size_list (x # xs) = Suc (size_list xs)"
-by (auto simp add: size_list_def)
+lemma size_list'_simps:
+ "size_list' [] = 0"
+ "size_list' (x # xs) = Suc (size_list' xs)"
+by (auto simp add: size_list'_def)
-declare size_list_simps[code_pred_def]
-declare size_list_def[symmetric, code_pred_inline]
+declare size_list'_simps[code_pred_def]
+declare size_list'_def[symmetric, code_pred_inline]
subsection {* Alternative rules for @{text list_all2} *}
--- a/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Tests.thy Thu Apr 24 00:08:48 2014 +0200
+++ b/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Tests.thy Thu Apr 24 00:23:38 2014 +0200
@@ -1077,12 +1077,12 @@
*)
subsection {* Inverting list functions *}
-code_pred [inductify, skip_proof] size_list .
-code_pred [new_random_dseq inductify] size_list .
-thm size_listP.equation
-thm size_listP.new_random_dseq_equation
+code_pred [inductify, skip_proof] size_list' .
+code_pred [new_random_dseq inductify] size_list' .
+thm size_list'P.equation
+thm size_list'P.new_random_dseq_equation
-values [new_random_dseq 2,3,10] 3 "{xs. size_listP (xs::nat list) (5::nat)}"
+values [new_random_dseq 2,3,10] 3 "{xs. size_list'P (xs::nat list) (5::nat)}"
code_pred (expected_modes: i => o => bool, o => i => bool, i => i => bool) [inductify, skip_proof] List.concat .
thm concatP.equation