tuned quotes, antiquotations and whitespace
authorhaftmann
Tue Jun 08 16:37:22 2010 +0200 (2010-06-08)
changeset 37388793618618f78
parent 37387 3581483cca6c
child 37389 09467cdfa198
tuned quotes, antiquotations and whitespace
src/HOL/Library/Binomial.thy
src/HOL/Library/Countable.thy
src/HOL/Library/Diagonalize.thy
src/HOL/Library/Efficient_Nat.thy
src/HOL/Library/Formal_Power_Series.thy
src/HOL/Nominal/Examples/Support.thy
src/HOL/SetInterval.thy
src/HOL/Sum_Type.thy
src/HOL/Tools/Qelim/cooper.ML
src/HOL/Tools/groebner.ML
src/HOL/Tools/lin_arith.ML
src/HOL/Tools/meson.ML
src/HOL/Tools/nat_numeral_simprocs.ML
src/HOL/Tools/refute.ML
src/HOL/ex/Dedekind_Real.thy
src/HOL/ex/Refute_Examples.thy
     1.1 --- a/src/HOL/Library/Binomial.thy	Tue Jun 08 16:37:19 2010 +0200
     1.2 +++ b/src/HOL/Library/Binomial.thy	Tue Jun 08 16:37:22 2010 +0200
     1.3 @@ -235,7 +235,7 @@
     1.4      have eq: "insert 0 {1 .. n} = {0..n}" by auto
     1.5      have th1: "(\<Prod>n\<in>{1\<Colon>nat..n}. a + of_nat n) =
     1.6        (\<Prod>n\<in>{0\<Colon>nat..n - 1}. a + 1 + of_nat n)"
     1.7 -      apply (rule setprod_reindex_cong[where f = "Suc"])
     1.8 +      apply (rule setprod_reindex_cong [where f = Suc])
     1.9        using n0 by (auto simp add: expand_fun_eq field_simps)
    1.10      have ?thesis apply (simp add: pochhammer_def)
    1.11      unfolding setprod_insert[OF th0, unfolded eq]
     2.1 --- a/src/HOL/Library/Countable.thy	Tue Jun 08 16:37:19 2010 +0200
     2.2 +++ b/src/HOL/Library/Countable.thy	Tue Jun 08 16:37:22 2010 +0200
     2.3 @@ -70,7 +70,7 @@
     2.4  
     2.5  text {* Sums *}
     2.6  
     2.7 -instance "+":: (countable, countable) countable
     2.8 +instance "+" :: (countable, countable) countable
     2.9    by (rule countable_classI [of "(\<lambda>x. case x of Inl a \<Rightarrow> to_nat (False, to_nat a)
    2.10                                       | Inr b \<Rightarrow> to_nat (True, to_nat b))"])
    2.11      (simp split: sum.split_asm)
     3.1 --- a/src/HOL/Library/Diagonalize.thy	Tue Jun 08 16:37:19 2010 +0200
     3.2 +++ b/src/HOL/Library/Diagonalize.thy	Tue Jun 08 16:37:22 2010 +0200
     3.3 @@ -81,7 +81,7 @@
     3.4  done
     3.5  
     3.6  
     3.7 -subsection {* Diagonalization: an injective embedding of two @{typ "nat"}s to one @{typ "nat"} *}
     3.8 +subsection {* Diagonalization: an injective embedding of two @{typ nat}s to one @{typ nat} *}
     3.9  
    3.10  definition diagonalize :: "nat \<Rightarrow> nat \<Rightarrow> nat" where
    3.11    "diagonalize m n = sum (m + n) + m"
     4.1 --- a/src/HOL/Library/Efficient_Nat.thy	Tue Jun 08 16:37:19 2010 +0200
     4.2 +++ b/src/HOL/Library/Efficient_Nat.thy	Tue Jun 08 16:37:22 2010 +0200
     4.3 @@ -11,7 +11,7 @@
     4.4  text {*
     4.5    When generating code for functions on natural numbers, the
     4.6    canonical representation using @{term "0::nat"} and
     4.7 -  @{term "Suc"} is unsuitable for computations involving large
     4.8 +  @{term Suc} is unsuitable for computations involving large
     4.9    numbers.  The efficiency of the generated code can be improved
    4.10    drastically by implementing natural numbers by target-language
    4.11    integers.  To do this, just include this theory.
    4.12 @@ -362,7 +362,7 @@
    4.13    Since natural numbers are implemented
    4.14    using integers in ML, the coercion function @{const "of_nat"} of type
    4.15    @{typ "nat \<Rightarrow> int"} is simply implemented by the identity function.
    4.16 -  For the @{const "nat"} function for converting an integer to a natural
    4.17 +  For the @{const nat} function for converting an integer to a natural
    4.18    number, we give a specific implementation using an ML function that
    4.19    returns its input value, provided that it is non-negative, and otherwise
    4.20    returns @{text "0"}.
     5.1 --- a/src/HOL/Library/Formal_Power_Series.thy	Tue Jun 08 16:37:19 2010 +0200
     5.2 +++ b/src/HOL/Library/Formal_Power_Series.thy	Tue Jun 08 16:37:22 2010 +0200
     5.3 @@ -2031,7 +2031,7 @@
     5.4      done
     5.5    also have "\<dots> = setsum (\<lambda>i. of_nat (i + 1) * a$(i+1) * (setsum (\<lambda>j. (b^ i)$j * of_nat (n - j + 1) * b$(n - j + 1)) {0..n})) {0.. n}"
     5.6      unfolding fps_deriv_nth
     5.7 -    apply (rule setsum_reindex_cong[where f="Suc"])
     5.8 +    apply (rule setsum_reindex_cong [where f = Suc])
     5.9      by (auto simp add: mult_assoc)
    5.10    finally have th0: "(fps_deriv (a oo b))$n = setsum (\<lambda>i. of_nat (i + 1) * a$(i+1) * (setsum (\<lambda>j. (b^ i)$j * of_nat (n - j + 1) * b$(n - j + 1)) {0..n})) {0.. n}" .
    5.11  
     6.1 --- a/src/HOL/Nominal/Examples/Support.thy	Tue Jun 08 16:37:19 2010 +0200
     6.2 +++ b/src/HOL/Nominal/Examples/Support.thy	Tue Jun 08 16:37:22 2010 +0200
     6.3 @@ -31,7 +31,7 @@
     6.4  
     6.5  text {* An atom is either even or odd. *}
     6.6  lemma even_or_odd:
     6.7 -  fixes n::"nat"
     6.8 +  fixes n :: nat
     6.9    shows "\<exists>i. (n = 2*i) \<or> (n=2*i+1)"
    6.10    by (induct n) (presburger)+
    6.11  
     7.1 --- a/src/HOL/SetInterval.thy	Tue Jun 08 16:37:19 2010 +0200
     7.2 +++ b/src/HOL/SetInterval.thy	Tue Jun 08 16:37:22 2010 +0200
     7.3 @@ -770,7 +770,7 @@
     7.4  qed
     7.5  
     7.6  lemma card_less_Suc2: "0 \<notin> M \<Longrightarrow> card {k. Suc k \<in> M \<and> k < i} = card {k \<in> M. k < Suc i}"
     7.7 -apply (rule card_bij_eq [of "Suc" _ _ "\<lambda>x. x - Suc 0"])
     7.8 +apply (rule card_bij_eq [of Suc _ _ "\<lambda>x. x - Suc 0"])
     7.9  apply simp
    7.10  apply fastsimp
    7.11  apply auto
     8.1 --- a/src/HOL/Sum_Type.thy	Tue Jun 08 16:37:19 2010 +0200
     8.2 +++ b/src/HOL/Sum_Type.thy	Tue Jun 08 16:37:22 2010 +0200
     8.3 @@ -17,21 +17,17 @@
     8.4  definition Inr_Rep :: "'b \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> bool \<Rightarrow> bool" where
     8.5    "Inr_Rep b x y p \<longleftrightarrow> y = b \<and> \<not> p"
     8.6  
     8.7 -global
     8.8 -
     8.9 -typedef (Sum) ('a, 'b) "+" (infixr "+" 10) = "{f. (\<exists>a. f = Inl_Rep (a::'a)) \<or> (\<exists>b. f = Inr_Rep (b::'b))}"
    8.10 +typedef (sum) ('a, 'b) "+" (infixr "+" 10) = "{f. (\<exists>a. f = Inl_Rep (a::'a)) \<or> (\<exists>b. f = Inr_Rep (b::'b))}"
    8.11    by auto
    8.12  
    8.13 -local
    8.14 -
    8.15 -lemma Inl_RepI: "Inl_Rep a \<in> Sum"
    8.16 -  by (auto simp add: Sum_def)
    8.17 +lemma Inl_RepI: "Inl_Rep a \<in> sum"
    8.18 +  by (auto simp add: sum_def)
    8.19  
    8.20 -lemma Inr_RepI: "Inr_Rep b \<in> Sum"
    8.21 -  by (auto simp add: Sum_def)
    8.22 +lemma Inr_RepI: "Inr_Rep b \<in> sum"
    8.23 +  by (auto simp add: sum_def)
    8.24  
    8.25 -lemma inj_on_Abs_Sum: "A \<subseteq> Sum \<Longrightarrow> inj_on Abs_Sum A"
    8.26 -  by (rule inj_on_inverseI, rule Abs_Sum_inverse) auto
    8.27 +lemma inj_on_Abs_sum: "A \<subseteq> sum \<Longrightarrow> inj_on Abs_sum A"
    8.28 +  by (rule inj_on_inverseI, rule Abs_sum_inverse) auto
    8.29  
    8.30  lemma Inl_Rep_inject: "inj_on Inl_Rep A"
    8.31  proof (rule inj_onI)
    8.32 @@ -49,28 +45,28 @@
    8.33    by (auto simp add: Inl_Rep_def Inr_Rep_def expand_fun_eq)
    8.34  
    8.35  definition Inl :: "'a \<Rightarrow> 'a + 'b" where
    8.36 -  "Inl = Abs_Sum \<circ> Inl_Rep"
    8.37 +  "Inl = Abs_sum \<circ> Inl_Rep"
    8.38  
    8.39  definition Inr :: "'b \<Rightarrow> 'a + 'b" where
    8.40 -  "Inr = Abs_Sum \<circ> Inr_Rep"
    8.41 +  "Inr = Abs_sum \<circ> Inr_Rep"
    8.42  
    8.43  lemma inj_Inl [simp]: "inj_on Inl A"
    8.44 -by (auto simp add: Inl_def intro!: comp_inj_on Inl_Rep_inject inj_on_Abs_Sum Inl_RepI)
    8.45 +by (auto simp add: Inl_def intro!: comp_inj_on Inl_Rep_inject inj_on_Abs_sum Inl_RepI)
    8.46  
    8.47  lemma Inl_inject: "Inl x = Inl y \<Longrightarrow> x = y"
    8.48  using inj_Inl by (rule injD)
    8.49  
    8.50  lemma inj_Inr [simp]: "inj_on Inr A"
    8.51 -by (auto simp add: Inr_def intro!: comp_inj_on Inr_Rep_inject inj_on_Abs_Sum Inr_RepI)
    8.52 +by (auto simp add: Inr_def intro!: comp_inj_on Inr_Rep_inject inj_on_Abs_sum Inr_RepI)
    8.53  
    8.54  lemma Inr_inject: "Inr x = Inr y \<Longrightarrow> x = y"
    8.55  using inj_Inr by (rule injD)
    8.56  
    8.57  lemma Inl_not_Inr: "Inl a \<noteq> Inr b"
    8.58  proof -
    8.59 -  from Inl_RepI [of a] Inr_RepI [of b] have "{Inl_Rep a, Inr_Rep b} \<subseteq> Sum" by auto
    8.60 -  with inj_on_Abs_Sum have "inj_on Abs_Sum {Inl_Rep a, Inr_Rep b}" .
    8.61 -  with Inl_Rep_not_Inr_Rep [of a b] inj_on_contraD have "Abs_Sum (Inl_Rep a) \<noteq> Abs_Sum (Inr_Rep b)" by auto
    8.62 +  from Inl_RepI [of a] Inr_RepI [of b] have "{Inl_Rep a, Inr_Rep b} \<subseteq> sum" by auto
    8.63 +  with inj_on_Abs_sum have "inj_on Abs_sum {Inl_Rep a, Inr_Rep b}" .
    8.64 +  with Inl_Rep_not_Inr_Rep [of a b] inj_on_contraD have "Abs_sum (Inl_Rep a) \<noteq> Abs_sum (Inr_Rep b)" by auto
    8.65    then show ?thesis by (simp add: Inl_def Inr_def)
    8.66  qed
    8.67  
    8.68 @@ -81,10 +77,10 @@
    8.69    assumes "\<And>x::'a. s = Inl x \<Longrightarrow> P"
    8.70      and "\<And>y::'b. s = Inr y \<Longrightarrow> P"
    8.71    shows P
    8.72 -proof (rule Abs_Sum_cases [of s])
    8.73 +proof (rule Abs_sum_cases [of s])
    8.74    fix f 
    8.75 -  assume "s = Abs_Sum f" and "f \<in> Sum"
    8.76 -  with assms show P by (auto simp add: Sum_def Inl_def Inr_def)
    8.77 +  assume "s = Abs_sum f" and "f \<in> sum"
    8.78 +  with assms show P by (auto simp add: sum_def Inl_def Inr_def)
    8.79  qed
    8.80  
    8.81  rep_datatype (sum) Inl Inr
     9.1 --- a/src/HOL/Tools/Qelim/cooper.ML	Tue Jun 08 16:37:19 2010 +0200
     9.2 +++ b/src/HOL/Tools/Qelim/cooper.ML	Tue Jun 08 16:37:22 2010 +0200
     9.3 @@ -37,7 +37,7 @@
     9.4     @{term "max :: int => _"}, @{term "max :: nat => _"},
     9.5     @{term "min :: int => _"}, @{term "min :: nat => _"},
     9.6     @{term "uminus :: int => _"}, (*@ {term "uminus :: nat => _"},*)
     9.7 -   @{term "Not"}, @{term "Suc"},
     9.8 +   @{term "Not"}, @{term Suc},
     9.9     @{term "Ex :: (int => _) => _"}, @{term "Ex :: (nat => _) => _"},
    9.10     @{term "All :: (int => _) => _"}, @{term "All :: (nat => _) => _"},
    9.11     @{term "nat"}, @{term "int"},
    9.12 @@ -726,7 +726,7 @@
    9.13   fun isnum t = case t of 
    9.14     Const(@{const_name Groups.zero},_) => true
    9.15   | Const(@{const_name Groups.one},_) => true
    9.16 - | @{term "Suc"}$s => isnum s
    9.17 + | @{term Suc}$s => isnum s
    9.18   | @{term "nat"}$s => isnum s
    9.19   | @{term "int"}$s => isnum s
    9.20   | Const(@{const_name Groups.uminus},_)$s => isnum s
    10.1 --- a/src/HOL/Tools/groebner.ML	Tue Jun 08 16:37:19 2010 +0200
    10.2 +++ b/src/HOL/Tools/groebner.ML	Tue Jun 08 16:37:22 2010 +0200
    10.3 @@ -698,7 +698,7 @@
    10.4  
    10.5  val holify_polynomial =
    10.6   let fun holify_varpow (v,n) =
    10.7 -  if n = 1 then v else ring_mk_pow v (Numeral.mk_cnumber @{ctyp "nat"} n)  (* FIXME *)
    10.8 +  if n = 1 then v else ring_mk_pow v (Numeral.mk_cnumber @{ctyp nat} n)  (* FIXME *)
    10.9   fun holify_monomial vars (c,m) =
   10.10    let val xps = map holify_varpow (filter (fn (_,n) => n <> 0) (vars ~~ m))
   10.11     in end_itlist ring_mk_mul (mk_const c :: xps)
    11.1 --- a/src/HOL/Tools/lin_arith.ML	Tue Jun 08 16:37:19 2010 +0200
    11.2 +++ b/src/HOL/Tools/lin_arith.ML	Tue Jun 08 16:37:22 2010 +0200
    11.3 @@ -461,7 +461,7 @@
    11.4      (* ?P ((?n::nat) mod (number_of ?k)) =
    11.5           ((number_of ?k = 0 --> ?P ?n) & (~ (number_of ?k = 0) -->
    11.6             (ALL i j. j < number_of ?k --> ?n = number_of ?k * i + j --> ?P j))) *)
    11.7 -    | (Const ("Divides.div_class.mod", Type ("fun", [Type ("nat", []), _])), [t1, t2]) =>
    11.8 +    | (Const ("Divides.div_class.mod", Type ("fun", [@{typ nat}, _])), [t1, t2]) =>
    11.9        let
   11.10          val rev_terms               = rev terms
   11.11          val zero                    = Const (@{const_name Groups.zero}, split_type)
   11.12 @@ -493,7 +493,7 @@
   11.13      (* ?P ((?n::nat) div (number_of ?k)) =
   11.14           ((number_of ?k = 0 --> ?P 0) & (~ (number_of ?k = 0) -->
   11.15             (ALL i j. j < number_of ?k --> ?n = number_of ?k * i + j --> ?P i))) *)
   11.16 -    | (Const ("Divides.div_class.div", Type ("fun", [Type ("nat", []), _])), [t1, t2]) =>
   11.17 +    | (Const ("Divides.div_class.div", Type ("fun", [@{typ nat}, _])), [t1, t2]) =>
   11.18        let
   11.19          val rev_terms               = rev terms
   11.20          val zero                    = Const (@{const_name Groups.zero}, split_type)
    12.1 --- a/src/HOL/Tools/meson.ML	Tue Jun 08 16:37:19 2010 +0200
    12.2 +++ b/src/HOL/Tools/meson.ML	Tue Jun 08 16:37:22 2010 +0200
    12.3 @@ -395,7 +395,7 @@
    12.4    since this code expects to be called on a clause form.*)
    12.5  val is_conn = member (op =)
    12.6      ["Trueprop", "op &", "op |", "op -->", "Not",
    12.7 -     "All", "Ex", "Ball", "Bex"];
    12.8 +     "All", "Ex", @{const_name Ball}, @{const_name Bex}];
    12.9  
   12.10  (*True if the term contains a function--not a logical connective--where the type
   12.11    of any argument contains bool.*)
    13.1 --- a/src/HOL/Tools/nat_numeral_simprocs.ML	Tue Jun 08 16:37:19 2010 +0200
    13.2 +++ b/src/HOL/Tools/nat_numeral_simprocs.ML	Tue Jun 08 16:37:22 2010 +0200
    13.3 @@ -97,7 +97,7 @@
    13.4  
    13.5  (*Split up a sum into the list of its constituent terms, on the way removing any
    13.6    Sucs and counting them.*)
    13.7 -fun dest_Suc_sum (Const ("Suc", _) $ t, (k,ts)) = dest_Suc_sum (t, (k+1,ts))
    13.8 +fun dest_Suc_sum (Const (@{const_name Suc}, _) $ t, (k,ts)) = dest_Suc_sum (t, (k+1,ts))
    13.9    | dest_Suc_sum (t, (k,ts)) = 
   13.10        let val (t1,t2) = dest_plus t
   13.11        in  dest_Suc_sum (t1, dest_Suc_sum (t2, (k,ts)))  end
    14.1 --- a/src/HOL/Tools/refute.ML	Tue Jun 08 16:37:19 2010 +0200
    14.2 +++ b/src/HOL/Tools/refute.ML	Tue Jun 08 16:37:22 2010 +0200
    14.3 @@ -657,14 +657,14 @@
    14.4        (* other optimizations *)
    14.5        | Const (@{const_name Finite_Set.card}, _) => t
    14.6        | Const (@{const_name Finite_Set.finite}, _) => t
    14.7 -      | Const (@{const_name Orderings.less}, Type ("fun", [Type ("nat", []),
    14.8 -        Type ("fun", [Type ("nat", []), Type ("bool", [])])])) => t
    14.9 -      | Const (@{const_name Groups.plus}, Type ("fun", [Type ("nat", []),
   14.10 -        Type ("fun", [Type ("nat", []), Type ("nat", [])])])) => t
   14.11 -      | Const (@{const_name Groups.minus}, Type ("fun", [Type ("nat", []),
   14.12 -        Type ("fun", [Type ("nat", []), Type ("nat", [])])])) => t
   14.13 -      | Const (@{const_name Groups.times}, Type ("fun", [Type ("nat", []),
   14.14 -        Type ("fun", [Type ("nat", []), Type ("nat", [])])])) => t
   14.15 +      | Const (@{const_name Orderings.less}, Type ("fun", [@{typ nat},
   14.16 +        Type ("fun", [@{typ nat}, Type ("bool", [])])])) => t
   14.17 +      | Const (@{const_name Groups.plus}, Type ("fun", [@{typ nat},
   14.18 +        Type ("fun", [@{typ nat}, @{typ nat}])])) => t
   14.19 +      | Const (@{const_name Groups.minus}, Type ("fun", [@{typ nat},
   14.20 +        Type ("fun", [@{typ nat}, @{typ nat}])])) => t
   14.21 +      | Const (@{const_name Groups.times}, Type ("fun", [@{typ nat},
   14.22 +        Type ("fun", [@{typ nat}, @{typ nat}])])) => t
   14.23        | Const (@{const_name List.append}, _) => t
   14.24  (* UNSOUND
   14.25        | Const (@{const_name lfp}, _) => t
   14.26 @@ -834,17 +834,17 @@
   14.27        | Const (@{const_name Finite_Set.card}, T) => collect_type_axioms T axs
   14.28        | Const (@{const_name Finite_Set.finite}, T) =>
   14.29          collect_type_axioms T axs
   14.30 -      | Const (@{const_name Orderings.less}, T as Type ("fun", [Type ("nat", []),
   14.31 -        Type ("fun", [Type ("nat", []), Type ("bool", [])])])) =>
   14.32 +      | Const (@{const_name Orderings.less}, T as Type ("fun", [@{typ nat},
   14.33 +        Type ("fun", [@{typ nat}, Type ("bool", [])])])) =>
   14.34            collect_type_axioms T axs
   14.35 -      | Const (@{const_name Groups.plus}, T as Type ("fun", [Type ("nat", []),
   14.36 -        Type ("fun", [Type ("nat", []), Type ("nat", [])])])) =>
   14.37 +      | Const (@{const_name Groups.plus}, T as Type ("fun", [@{typ nat},
   14.38 +        Type ("fun", [@{typ nat}, @{typ nat}])])) =>
   14.39            collect_type_axioms T axs
   14.40 -      | Const (@{const_name Groups.minus}, T as Type ("fun", [Type ("nat", []),
   14.41 -        Type ("fun", [Type ("nat", []), Type ("nat", [])])])) =>
   14.42 +      | Const (@{const_name Groups.minus}, T as Type ("fun", [@{typ nat},
   14.43 +        Type ("fun", [@{typ nat}, @{typ nat}])])) =>
   14.44            collect_type_axioms T axs
   14.45 -      | Const (@{const_name Groups.times}, T as Type ("fun", [Type ("nat", []),
   14.46 -        Type ("fun", [Type ("nat", []), Type ("nat", [])])])) =>
   14.47 +      | Const (@{const_name Groups.times}, T as Type ("fun", [@{typ nat},
   14.48 +        Type ("fun", [@{typ nat}, @{typ nat}])])) =>
   14.49            collect_type_axioms T axs
   14.50        | Const (@{const_name List.append}, T) => collect_type_axioms T axs
   14.51  (* UNSOUND
   14.52 @@ -2654,7 +2654,7 @@
   14.53      case t of
   14.54        Const (@{const_name Finite_Set.card},
   14.55          Type ("fun", [Type ("fun", [T, Type ("bool", [])]),
   14.56 -                      Type ("nat", [])])) =>
   14.57 +                      @{typ nat}])) =>
   14.58        let
   14.59          (* interpretation -> int *)
   14.60          fun number_of_elements (Node xs) =
   14.61 @@ -2670,7 +2670,7 @@
   14.62            | number_of_elements (Leaf _) =
   14.63            raise REFUTE ("Finite_Set_card_interpreter",
   14.64              "interpretation for set type is a leaf")
   14.65 -        val size_of_nat = size_of_type thy model (Type ("nat", []))
   14.66 +        val size_of_nat = size_of_type thy model (@{typ nat})
   14.67          (* takes an interpretation for a set and returns an interpretation *)
   14.68          (* for a 'nat' denoting the set's cardinality                      *)
   14.69          (* interpretation -> interpretation *)
   14.70 @@ -2730,10 +2730,10 @@
   14.71  
   14.72    fun Nat_less_interpreter thy model args t =
   14.73      case t of
   14.74 -      Const (@{const_name Orderings.less}, Type ("fun", [Type ("nat", []),
   14.75 -        Type ("fun", [Type ("nat", []), Type ("bool", [])])])) =>
   14.76 +      Const (@{const_name Orderings.less}, Type ("fun", [@{typ nat},
   14.77 +        Type ("fun", [@{typ nat}, Type ("bool", [])])])) =>
   14.78        let
   14.79 -        val size_of_nat = size_of_type thy model (Type ("nat", []))
   14.80 +        val size_of_nat = size_of_type thy model (@{typ nat})
   14.81          (* the 'n'-th nat is not less than the first 'n' nats, while it *)
   14.82          (* is less than the remaining 'size_of_nat - n' nats            *)
   14.83          (* int -> interpretation *)
   14.84 @@ -2753,10 +2753,10 @@
   14.85  
   14.86    fun Nat_plus_interpreter thy model args t =
   14.87      case t of
   14.88 -      Const (@{const_name Groups.plus}, Type ("fun", [Type ("nat", []),
   14.89 -        Type ("fun", [Type ("nat", []), Type ("nat", [])])])) =>
   14.90 +      Const (@{const_name Groups.plus}, Type ("fun", [@{typ nat},
   14.91 +        Type ("fun", [@{typ nat}, @{typ nat}])])) =>
   14.92        let
   14.93 -        val size_of_nat = size_of_type thy model (Type ("nat", []))
   14.94 +        val size_of_nat = size_of_type thy model (@{typ nat})
   14.95          (* int -> int -> interpretation *)
   14.96          fun plus m n =
   14.97            let
   14.98 @@ -2784,10 +2784,10 @@
   14.99  
  14.100    fun Nat_minus_interpreter thy model args t =
  14.101      case t of
  14.102 -      Const (@{const_name Groups.minus}, Type ("fun", [Type ("nat", []),
  14.103 -        Type ("fun", [Type ("nat", []), Type ("nat", [])])])) =>
  14.104 +      Const (@{const_name Groups.minus}, Type ("fun", [@{typ nat},
  14.105 +        Type ("fun", [@{typ nat}, @{typ nat}])])) =>
  14.106        let
  14.107 -        val size_of_nat = size_of_type thy model (Type ("nat", []))
  14.108 +        val size_of_nat = size_of_type thy model (@{typ nat})
  14.109          (* int -> int -> interpretation *)
  14.110          fun minus m n =
  14.111            let
  14.112 @@ -2812,10 +2812,10 @@
  14.113  
  14.114    fun Nat_times_interpreter thy model args t =
  14.115      case t of
  14.116 -      Const (@{const_name Groups.times}, Type ("fun", [Type ("nat", []),
  14.117 -        Type ("fun", [Type ("nat", []), Type ("nat", [])])])) =>
  14.118 +      Const (@{const_name Groups.times}, Type ("fun", [@{typ nat},
  14.119 +        Type ("fun", [@{typ nat}, @{typ nat}])])) =>
  14.120        let
  14.121 -        val size_of_nat = size_of_type thy model (Type ("nat", []))
  14.122 +        val size_of_nat = size_of_type thy model (@{typ nat})
  14.123          (* nat -> nat -> interpretation *)
  14.124          fun mult m n =
  14.125            let
    15.1 --- a/src/HOL/ex/Dedekind_Real.thy	Tue Jun 08 16:37:19 2010 +0200
    15.2 +++ b/src/HOL/ex/Dedekind_Real.thy	Tue Jun 08 16:37:22 2010 +0200
    15.3 @@ -2006,7 +2006,7 @@
    15.4  qed
    15.5  
    15.6  text {*
    15.7 -  There must be other proofs, e.g. @{text "Suc"} of the largest
    15.8 +  There must be other proofs, e.g. @{text Suc} of the largest
    15.9    integer in the cut representing @{text "x"}.
   15.10  *}
   15.11  
    16.1 --- a/src/HOL/ex/Refute_Examples.thy	Tue Jun 08 16:37:19 2010 +0200
    16.2 +++ b/src/HOL/ex/Refute_Examples.thy	Tue Jun 08 16:37:22 2010 +0200
    16.3 @@ -774,7 +774,7 @@
    16.4  oops
    16.5  
    16.6  lemma "P Suc"
    16.7 -  refute  -- {* @{term "Suc"} is a partial function (regardless of the size
    16.8 +  refute  -- {* @{term Suc} is a partial function (regardless of the size
    16.9                  of the model), hence @{term "P Suc"} is undefined, hence no
   16.10                  model will be found *}
   16.11  oops