1.1 --- a/src/HOL/ex/Reflected_Presburger.thy	Fri Sep 23 20:13:54 2005 +0200
     1.2 +++ b/src/HOL/ex/Reflected_Presburger.thy	Fri Sep 23 21:02:13 2005 +0200
     1.3 @@ -4,7 +4,7 @@
     1.4  
     1.5  A formalization of quantifier elimination for Presburger arithmetic
     1.6  based on a generic quantifier elimination algorithm and Cooper's
     1.7 -methos to eliminate on \<exists>. *)
     1.8 +method to eliminate on \<exists>. *)
     1.9  
    1.10  header {* Quantifier elimination for Presburger arithmetic *}
    1.11  
    1.12 @@ -21,7 +21,7 @@
    1.13    | Sub intterm intterm
    1.14    | Mult intterm intterm
    1.15  
    1.16 -(* interpretatation of intterms , takes bound variables and free variables *)
    1.17 +(* interpretation of intterms, takes bound variables and free variables *)
    1.18  consts I_intterm :: "int list \<Rightarrow> intterm \<Rightarrow> int"
    1.19  primrec 
    1.20  "I_intterm ats (Cst b) = b"
    1.21 @@ -31,7 +31,7 @@
    1.22  "I_intterm ats (Sub it1 it2) = (I_intterm ats it1) - (I_intterm ats it2)"
    1.23  "I_intterm ats (Mult it1 it2) = (I_intterm ats it1) * (I_intterm ats it2)"
    1.24  
    1.25 -(*Shadow syntax for Presburger formulae *)
    1.26 +(* Shadow syntax for Presburger formulae *)
    1.27  datatype QF = 
    1.28     Lt intterm intterm
    1.29    |Gt intterm intterm
    1.30 @@ -49,7 +49,7 @@
    1.31    |QAll QF
    1.32    |QEx QF
    1.33  
    1.34 -(* Interpretation of Presburger  formulae *)
    1.35 +(* Interpretation of Presburger formulae *)
    1.36  consts qinterp :: "int list \<Rightarrow> QF \<Rightarrow> bool"
    1.37  primrec
    1.38  "qinterp ats (Lt it1 it2) = (I_intterm ats it1 < I_intterm ats it2)"
    1.39 @@ -70,8 +70,8 @@
    1.40  
    1.41  (* quantifier elimination based on qe, quantifier elimination for an
    1.42     existential formula, with quantifier free body 
    1.43 -   Since quantifier elimination for one formula is allowed to fail, 
    1.44 -   the reult is of type QF option *)
    1.45 +   Since quantifier elimination for one formula is allowed to fail,
    1.46 +   the result is of type QF option *)
    1.47  
    1.48  consts lift_bin:: "('a \<Rightarrow> 'a \<Rightarrow> 'b) \<times> 'a option \<times> 'a option \<Rightarrow> 'b option"
    1.49  recdef lift_bin "measure (\<lambda>(c,a,b). size a)"
    1.50 @@ -565,8 +565,8 @@
    1.51    shows "I_intterm (x#ats) r = I_intterm (y#ats) r"
    1.52  using lin
    1.53  by (induct r rule: islinintterm.induct) (simp_all add: nth_pos2)
    1.54 -(* a simple version of a general theorem: Interpretation doese not depend 
    1.55 -   on the first variable if it doese not occur in the term *)
    1.56 +(* a simple version of a general theorem: Interpretation does not depend 
    1.57 +   on the first variable if it does not occur in the term *)
    1.58  
    1.59  lemma linterm_novar0:
    1.60    assumes lin: "islintn (n,t)"