# HG changeset patch
# User webertj
# Date 1127502133 -7200
# Node ID 77e026bef398430a134daeecfea042f79c12d443
# Parent  7725da65f8e03c09ecae7fda8b8a54f4da04c436
some typos in comments fixed

diff -r 7725da65f8e0 -r 77e026bef398 src/HOL/ex/Reflected_Presburger.thy
--- a/src/HOL/ex/Reflected_Presburger.thy	Fri Sep 23 20:13:54 2005 +0200
+++ b/src/HOL/ex/Reflected_Presburger.thy	Fri Sep 23 21:02:13 2005 +0200
@@ -4,7 +4,7 @@
 
 A formalization of quantifier elimination for Presburger arithmetic
 based on a generic quantifier elimination algorithm and Cooper's
-methos to eliminate on \<exists>. *)
+method to eliminate on \<exists>. *)
 
 header {* Quantifier elimination for Presburger arithmetic *}
 
@@ -21,7 +21,7 @@
   | Sub intterm intterm
   | Mult intterm intterm
 
-(* interpretatation of intterms , takes bound variables and free variables *)
+(* interpretation of intterms, takes bound variables and free variables *)
 consts I_intterm :: "int list \<Rightarrow> intterm \<Rightarrow> int"
 primrec 
 "I_intterm ats (Cst b) = b"
@@ -31,7 +31,7 @@
 "I_intterm ats (Sub it1 it2) = (I_intterm ats it1) - (I_intterm ats it2)"
 "I_intterm ats (Mult it1 it2) = (I_intterm ats it1) * (I_intterm ats it2)"
 
-(*Shadow syntax for Presburger formulae *)
+(* Shadow syntax for Presburger formulae *)
 datatype QF = 
    Lt intterm intterm
   |Gt intterm intterm
@@ -49,7 +49,7 @@
   |QAll QF
   |QEx QF
 
-(* Interpretation of Presburger  formulae *)
+(* Interpretation of Presburger formulae *)
 consts qinterp :: "int list \<Rightarrow> QF \<Rightarrow> bool"
 primrec
 "qinterp ats (Lt it1 it2) = (I_intterm ats it1 < I_intterm ats it2)"
@@ -70,8 +70,8 @@
 
 (* quantifier elimination based on qe, quantifier elimination for an
    existential formula, with quantifier free body 
-   Since quantifier elimination for one formula is allowed to fail, 
-   the reult is of type QF option *)
+   Since quantifier elimination for one formula is allowed to fail,
+   the result is of type QF option *)
 
 consts lift_bin:: "('a \<Rightarrow> 'a \<Rightarrow> 'b) \<times> 'a option \<times> 'a option \<Rightarrow> 'b option"
 recdef lift_bin "measure (\<lambda>(c,a,b). size a)"
@@ -565,8 +565,8 @@
   shows "I_intterm (x#ats) r = I_intterm (y#ats) r"
 using lin
 by (induct r rule: islinintterm.induct) (simp_all add: nth_pos2)
-(* a simple version of a general theorem: Interpretation doese not depend 
-   on the first variable if it doese not occur in the term *)
+(* a simple version of a general theorem: Interpretation does not depend 
+   on the first variable if it does not occur in the term *)
 
 lemma linterm_novar0:
   assumes lin: "islintn (n,t)"