# HG changeset patch
# User haftmann
# Date 1497938516 -7200
# Node ID 6e4904863d2a9068a51320a211e298d8559503b8
# Parent  ea7c2a245b84803aebfa3e09c69d5a2bde140451
spelling

diff -r ea7c2a245b84 -r 6e4904863d2a src/HOL/Decision_Procs/MIR.thy
--- a/src/HOL/Decision_Procs/MIR.thy	Mon Jun 19 21:33:29 2017 +0200
+++ b/src/HOL/Decision_Procs/MIR.thy	Tue Jun 20 08:01:56 2017 +0200
@@ -2239,7 +2239,7 @@
 lemma dvd1_eq1: "x >0 \<Longrightarrow> (x::int) dvd 1 = (x = 1)" by auto
 
 consts
-  a_\<beta> :: "fm \<Rightarrow> int \<Rightarrow> fm" (* adjusts the coeffitients of a formula *)
+  a_\<beta> :: "fm \<Rightarrow> int \<Rightarrow> fm" (* adjusts the coefficients of a formula *)
   d_\<beta> :: "fm \<Rightarrow> int \<Rightarrow> bool" (* tests if all coeffs c of c divide a given l*)
   \<zeta>  :: "fm \<Rightarrow> int" (* computes the lcm of all coefficients of x*)
   \<beta> :: "fm \<Rightarrow> num list"