src/HOL/Nitpick.thy

--- a/src/HOL/Nitpick.thy	Wed Apr 23 10:23:26 2014 +0200
+++ b/src/HOL/Nitpick.thy	Wed Apr 23 10:23:27 2014 +0200
@@ -113,9 +113,8 @@
 
 declare nat.case [nitpick_simp del]
 
-lemma list_size_simp [nitpick_simp]:
-"list_size f xs = (if xs = [] then 0
-                   else Suc (f (hd xs) + list_size f (tl xs)))"
+lemma size_list_simp [nitpick_simp]:
+"size_list f xs = (if xs = [] then 0 else Suc (f (hd xs) + size_list f (tl xs)))"
 "size xs = (if xs = [] then 0 else Suc (size (tl xs)))"
 by (cases xs) auto
 
@@ -145,8 +144,9 @@
 definition Frac :: "int \<times> int \<Rightarrow> bool" where
 "Frac \<equiv> \<lambda>(a, b). b > 0 \<and> int_gcd a b = 1"
 
-axiomatization Abs_Frac :: "int \<times> int \<Rightarrow> 'a"
-           and Rep_Frac :: "'a \<Rightarrow> int \<times> int"
+axiomatization
+  Abs_Frac :: "int \<times> int \<Rightarrow> 'a" and
+  Rep_Frac :: "'a \<Rightarrow> int \<times> int"
 
 definition zero_frac :: 'a where
 "zero_frac \<equiv> Abs_Frac (0, 1)"
@@ -244,7 +244,7 @@
 hide_fact (open) Ex1_unfold rtrancl_unfold rtranclp_unfold tranclp_unfold
     prod_def refl'_def wf'_def card'_def setsum'_def
     fold_graph'_def The_psimp Eps_psimp case_unit_unfold case_nat_unfold
-    list_size_simp nat_gcd_def nat_lcm_def int_gcd_def int_lcm_def Frac_def
+    size_list_simp nat_gcd_def nat_lcm_def int_gcd_def int_lcm_def Frac_def
     zero_frac_def one_frac_def num_def denom_def norm_frac_def frac_def
     plus_frac_def times_frac_def uminus_frac_def number_of_frac_def
     inverse_frac_def less_frac_def less_eq_frac_def of_frac_def wf_wfrec'_def