src/HOL/Nitpick.thy
 changeset 56643 41d3596d8a64 parent 55642 63beb38e9258 child 57231 dca8d06ecbba
```     1.1 --- a/src/HOL/Nitpick.thy	Wed Apr 23 10:23:26 2014 +0200
1.2 +++ b/src/HOL/Nitpick.thy	Wed Apr 23 10:23:27 2014 +0200
1.3 @@ -113,9 +113,8 @@
1.4
1.5  declare nat.case [nitpick_simp del]
1.6
1.7 -lemma list_size_simp [nitpick_simp]:
1.8 -"list_size f xs = (if xs = [] then 0
1.9 -                   else Suc (f (hd xs) + list_size f (tl xs)))"
1.10 +lemma size_list_simp [nitpick_simp]:
1.11 +"size_list f xs = (if xs = [] then 0 else Suc (f (hd xs) + size_list f (tl xs)))"
1.12  "size xs = (if xs = [] then 0 else Suc (size (tl xs)))"
1.13  by (cases xs) auto
1.14
1.15 @@ -145,8 +144,9 @@
1.16  definition Frac :: "int \<times> int \<Rightarrow> bool" where
1.17  "Frac \<equiv> \<lambda>(a, b). b > 0 \<and> int_gcd a b = 1"
1.18
1.19 -axiomatization Abs_Frac :: "int \<times> int \<Rightarrow> 'a"
1.20 -           and Rep_Frac :: "'a \<Rightarrow> int \<times> int"
1.21 +axiomatization
1.22 +  Abs_Frac :: "int \<times> int \<Rightarrow> 'a" and
1.23 +  Rep_Frac :: "'a \<Rightarrow> int \<times> int"
1.24
1.25  definition zero_frac :: 'a where
1.26  "zero_frac \<equiv> Abs_Frac (0, 1)"
1.27 @@ -244,7 +244,7 @@
1.28  hide_fact (open) Ex1_unfold rtrancl_unfold rtranclp_unfold tranclp_unfold
1.29      prod_def refl'_def wf'_def card'_def setsum'_def
1.30      fold_graph'_def The_psimp Eps_psimp case_unit_unfold case_nat_unfold
1.31 -    list_size_simp nat_gcd_def nat_lcm_def int_gcd_def int_lcm_def Frac_def
1.32 +    size_list_simp nat_gcd_def nat_lcm_def int_gcd_def int_lcm_def Frac_def
1.33      zero_frac_def one_frac_def num_def denom_def norm_frac_def frac_def
1.34      plus_frac_def times_frac_def uminus_frac_def number_of_frac_def
1.35      inverse_frac_def less_frac_def less_eq_frac_def of_frac_def wf_wfrec'_def
```