# HG changeset patch
# User wenzelm
# Date 1393856040 -3600
# Node ID b11b358fec5762373d5bc8af533d59d7fdd19cf5
# Parent  6478b12b7297ee118950100211c3160531f25c54# Parent  c871a2e751ec8a6da32d35bc6d8de030dafae615
merged;

diff -r 6478b12b7297 -r b11b358fec57 Admin/isatest/settings/at-poly-test
--- a/Admin/isatest/settings/at-poly-test	Mon Mar 03 14:22:35 2014 +0100
+++ b/Admin/isatest/settings/at-poly-test	Mon Mar 03 15:14:00 2014 +0100
@@ -2,8 +2,8 @@
 
 init_components /home/isabelle/contrib "$HOME/admin/components/main"
 
-  POLYML_HOME="/home/polyml/polyml-5.5.1"
-  ML_SYSTEM="polyml-5.5.1"
+  POLYML_HOME="/home/polyml/polyml-svn"
+  ML_SYSTEM="polyml-5.5.2"
   ML_PLATFORM="x86-linux"
   ML_HOME="$POLYML_HOME/$ML_PLATFORM"
   ML_OPTIONS="-H 500 --gcthreads 1"
diff -r 6478b12b7297 -r b11b358fec57 src/Doc/JEdit/JEdit.thy
--- a/src/Doc/JEdit/JEdit.thy	Mon Mar 03 14:22:35 2014 +0100
+++ b/src/Doc/JEdit/JEdit.thy	Mon Mar 03 15:14:00 2014 +0100
@@ -282,7 +282,7 @@
   \emph{all} platforms.\footnote{Isabelle on Windows uses Cygwin
   file-system access.}  Moreover, environment variables from the
   Isabelle process may be used freely, e.g.\ @{file
-  "$ISABELLE_HOME/etc/symbols"} or @{file "$POLYML_HOME/README"}.
+  "$ISABELLE_HOME/etc/symbols"} or @{file_unchecked "$POLYML_HOME/README"}.
   There are special shortcuts: @{file "~"} for @{file "$USER_HOME"}
   and @{file "~~"} for @{file "$ISABELLE_HOME"}.
 
diff -r 6478b12b7297 -r b11b358fec57 src/HOL/Decision_Procs/Cooper.thy
--- a/src/HOL/Decision_Procs/Cooper.thy	Mon Mar 03 14:22:35 2014 +0100
+++ b/src/HOL/Decision_Procs/Cooper.thy	Mon Mar 03 15:14:00 2014 +0100
@@ -3,14 +3,17 @@
 *)
 
 theory Cooper
-imports Complex_Main "~~/src/HOL/Library/Code_Target_Numeral" "~~/src/HOL/Library/Old_Recdef"
+imports
+  Complex_Main
+  "~~/src/HOL/Library/Code_Target_Numeral"
+  "~~/src/HOL/Library/Old_Recdef"
 begin
 
 (* Periodicity of dvd *)
 
-  (*********************************************************************************)
-  (****                            SHADOW SYNTAX AND SEMANTICS                  ****)
-  (*********************************************************************************)
+(*********************************************************************************)
+(****                            SHADOW SYNTAX AND SEMANTICS                  ****)
+(*********************************************************************************)
 
 datatype num = C int | Bound nat | CN nat int num | Neg num | Add num num| Sub num num
   | Mul int num
@@ -207,7 +210,7 @@
 
 lemma subst0_I:
   assumes qfp: "qfree p"
-  shows "Ifm bbs (b#bs) (subst0 a p) = Ifm bbs ((Inum (b#bs) a)#bs) p"
+  shows "Ifm bbs (b # bs) (subst0 a p) = Ifm bbs (Inum (b # bs) a # bs) p"
   using qfp numsubst0_I[where b="b" and bs="bs" and a="a"]
   by (induct p) (simp_all add: gr0_conv_Suc)
 
@@ -240,12 +243,12 @@
 
 lemma decrnum:
   assumes nb: "numbound0 t"
-  shows "Inum (x#bs) t = Inum bs (decrnum t)"
+  shows "Inum (x # bs) t = Inum bs (decrnum t)"
   using nb by (induct t rule: decrnum.induct) (auto simp add: gr0_conv_Suc)
 
 lemma decr:
   assumes nb: "bound0 p"
-  shows "Ifm bbs (x#bs) p = Ifm bbs bs (decr p)"
+  shows "Ifm bbs (x # bs) p = Ifm bbs bs (decr p)"
   using nb by (induct p rule: decr.induct) (simp_all add: gr0_conv_Suc decrnum)
 
 lemma decr_qf: "bound0 p \<Longrightarrow> qfree (decr p)"
@@ -290,18 +293,20 @@
 definition djf :: "('a \<Rightarrow> fm) \<Rightarrow> 'a \<Rightarrow> fm \<Rightarrow> fm"
 where
   "djf f p q =
-    (if q = T then T
-     else if q = F then f p
-     else (let fp = f p in case fp of T \<Rightarrow> T | F \<Rightarrow> q | _ \<Rightarrow> Or (f p) q))"
+   (if q = T then T
+    else if q = F then f p
+    else
+      let fp = f p
+      in case fp of T \<Rightarrow> T | F \<Rightarrow> q | _ \<Rightarrow> Or (f p) q)"
 
 definition evaldjf :: "('a \<Rightarrow> fm) \<Rightarrow> 'a list \<Rightarrow> fm"
   where "evaldjf f ps = foldr (djf f) ps F"
 
 lemma djf_Or: "Ifm bbs bs (djf f p q) = Ifm bbs bs (Or (f p) q)"
-  by (cases "q=T", simp add: djf_def,cases "q=F",simp add: djf_def)
+  by (cases "q=T", simp add: djf_def, cases "q = F", simp add: djf_def)
     (cases "f p", simp_all add: Let_def djf_def)
 
-lemma evaldjf_ex: "Ifm bbs bs (evaldjf f ps) = (\<exists>p \<in> set ps. Ifm bbs bs (f p))"
+lemma evaldjf_ex: "Ifm bbs bs (evaldjf f ps) \<longleftrightarrow> (\<exists>p \<in> set ps. Ifm bbs bs (f p))"
   by (induct ps) (simp_all add: evaldjf_def djf_Or)
 
 lemma evaldjf_bound0:
@@ -320,8 +325,8 @@
 | "disjuncts F = []"
 | "disjuncts p = [p]"
 
-lemma disjuncts: "(\<exists>q \<in> set (disjuncts p). Ifm bbs bs q) = Ifm bbs bs p"
- by (induct p rule: disjuncts.induct) auto
+lemma disjuncts: "(\<exists>q \<in> set (disjuncts p). Ifm bbs bs q) \<longleftrightarrow> Ifm bbs bs p"
+  by (induct p rule: disjuncts.induct) auto
 
 lemma disjuncts_nb:
   assumes nb: "bound0 p"
@@ -329,7 +334,7 @@
 proof -
   from nb have "list_all bound0 (disjuncts p)"
     by (induct p rule: disjuncts.induct) auto
-  thus ?thesis by (simp only: list_all_iff)
+  then show ?thesis by (simp only: list_all_iff)
 qed
 
 lemma disjuncts_qf:
@@ -338,7 +343,7 @@
 proof -
   from qf have "list_all qfree (disjuncts p)"
     by (induct p rule: disjuncts.induct) auto
-  thus ?thesis by (simp only: list_all_iff)
+  then show ?thesis by (simp only: list_all_iff)
 qed
 
 definition DJ :: "(fm \<Rightarrow> fm) \<Rightarrow> fm \<Rightarrow> fm"
@@ -372,8 +377,8 @@
 qed
 
 lemma DJ_qe:
-  assumes qe: "\<forall>bs p. qfree p \<longrightarrow> qfree (qe p) \<and> (Ifm bbs bs (qe p) = Ifm bbs bs (E p))"
-  shows "\<forall>bs p. qfree p \<longrightarrow> qfree (DJ qe p) \<and> (Ifm bbs bs ((DJ qe p)) = Ifm bbs bs (E p))"
+  assumes qe: "\<forall>bs p. qfree p \<longrightarrow> qfree (qe p) \<and> Ifm bbs bs (qe p) = Ifm bbs bs (E p)"
+  shows "\<forall>bs p. qfree p \<longrightarrow> qfree (DJ qe p) \<and> Ifm bbs bs ((DJ qe p)) = Ifm bbs bs (E p)"
 proof clarify
   fix p :: fm
   fix bs
@@ -449,7 +454,8 @@
 apply pat_completeness apply auto*)
 
 lemma numadd: "Inum bs (numadd (t,s)) = Inum bs (Add t s)"
-  apply (induct t s rule: numadd.induct, simp_all add: Let_def)
+  apply (induct t s rule: numadd.induct)
+  apply (simp_all add: Let_def)
   apply (case_tac "c1 + c2 = 0")
   apply (case_tac "n1 \<le> n2")
   apply simp_all
@@ -549,7 +555,7 @@
        else Or p q)"
 
 lemma disj: "Ifm bbs bs (disj p q) = Ifm bbs bs (Or p q)"
-  by (cases "p=T \<or> q=T", simp_all add: disj_def) (cases p, simp_all)
+  by (cases "p = T \<or> q = T", simp_all add: disj_def) (cases p, simp_all)
 
 lemma disj_qf: "qfree p \<Longrightarrow> qfree q \<Longrightarrow> qfree (disj p q)"
   using disj_def by auto
@@ -575,25 +581,25 @@
   using imp_def by (cases "p = F \<or> q = T", simp_all add: imp_def, cases p) simp_all
 
 definition iff :: "fm \<Rightarrow> fm \<Rightarrow> fm"
-  where
-    "iff p q =
-      (if p = q then T
-       else if p = not q \<or> not p = q then F
-       else if p = F then not q
-       else if q = F then not p
-       else if p = T then q
-       else if q = T then p
-       else Iff p q)"
+where
+  "iff p q =
+    (if p = q then T
+     else if p = not q \<or> not p = q then F
+     else if p = F then not q
+     else if q = F then not p
+     else if p = T then q
+     else if q = T then p
+     else Iff p q)"
 
 lemma iff: "Ifm bbs bs (iff p q) = Ifm bbs bs (Iff p q)"
-  by (unfold iff_def,cases "p=q", simp,cases "p=not q", simp add:not)
-    (cases "not p= q", auto simp add:not)
+  by (unfold iff_def, cases "p = q", simp, cases "p = not q", simp add: not)
+    (cases "not p = q", auto simp add: not)
 
-lemma iff_qf: "\<lbrakk>qfree p ; qfree q\<rbrakk> \<Longrightarrow> qfree (iff p q)"
-  by (unfold iff_def,cases "p=q", auto simp add: not_qf)
+lemma iff_qf: "qfree p \<Longrightarrow> qfree q \<Longrightarrow> qfree (iff p q)"
+  by (unfold iff_def, cases "p = q", auto simp add: not_qf)
 
-lemma iff_nb: "\<lbrakk>bound0 p ; bound0 q\<rbrakk> \<Longrightarrow> bound0 (iff p q)"
-  using iff_def by (unfold iff_def,cases "p=q", auto simp add: not_bn)
+lemma iff_nb: "bound0 p \<Longrightarrow> bound0 q \<Longrightarrow> bound0 (iff p q)"
+  using iff_def by (unfold iff_def, cases "p = q", auto simp add: not_bn)
 
 function (sequential) simpfm :: "fm \<Rightarrow> fm"
 where
@@ -609,12 +615,12 @@
 | "simpfm (Eq a) = (let a' = simpnum a in case a' of C v \<Rightarrow> if (v = 0)  then T else F | _ \<Rightarrow> Eq a')"
 | "simpfm (NEq a) = (let a' = simpnum a in case a' of C v \<Rightarrow> if (v \<noteq> 0)  then T else F | _ \<Rightarrow> NEq a')"
 | "simpfm (Dvd i a) =
-    (if i=0 then simpfm (Eq a)
-     else if (abs i = 1) then T
+    (if i = 0 then simpfm (Eq a)
+     else if abs i = 1 then T
      else let a' = simpnum a in case a' of C v \<Rightarrow> if (i dvd v)  then T else F | _ \<Rightarrow> Dvd i a')"
 | "simpfm (NDvd i a) =
-    (if i=0 then simpfm (NEq a)
-     else if (abs i = 1) then F
+    (if i = 0 then simpfm (NEq a)
+     else if abs i = 1 then F
      else let a' = simpnum a in case a' of C v \<Rightarrow> if (\<not>(i dvd v)) then T else F | _ \<Rightarrow> NDvd i a')"
 | "simpfm p = p"
   by pat_completeness auto
@@ -625,67 +631,67 @@
   case (6 a)
   let ?sa = "simpnum a"
   from simpnum_ci have sa: "Inum bs ?sa = Inum bs a" by simp
-  { fix v assume "?sa = C v" hence ?case using sa by simp }
+  { fix v assume "?sa = C v" then have ?case using sa by simp }
   moreover {
     assume "\<not> (\<exists>v. ?sa = C v)"
-    hence ?case using sa by (cases ?sa) (simp_all add: Let_def)
+    then have ?case using sa by (cases ?sa) (simp_all add: Let_def)
   }
   ultimately show ?case by blast
 next
   case (7 a)
   let ?sa = "simpnum a"
   from simpnum_ci have sa: "Inum bs ?sa = Inum bs a" by simp
-  { fix v assume "?sa = C v" hence ?case using sa by simp }
+  { fix v assume "?sa = C v" then have ?case using sa by simp }
   moreover {
     assume "\<not> (\<exists>v. ?sa = C v)"
-    hence ?case using sa by (cases ?sa) (simp_all add: Let_def)
+    then have ?case using sa by (cases ?sa) (simp_all add: Let_def)
   }
   ultimately show ?case by blast
 next
   case (8 a)
   let ?sa = "simpnum a"
   from simpnum_ci have sa: "Inum bs ?sa = Inum bs a" by simp
-  { fix v assume "?sa = C v" hence ?case using sa by simp }
+  { fix v assume "?sa = C v" then have ?case using sa by simp }
   moreover {
     assume "\<not> (\<exists>v. ?sa = C v)"
-    hence ?case using sa by (cases ?sa) (simp_all add: Let_def)
+    then have ?case using sa by (cases ?sa) (simp_all add: Let_def)
   }
   ultimately show ?case by blast
 next
   case (9 a)
   let ?sa = "simpnum a"
   from simpnum_ci have sa: "Inum bs ?sa = Inum bs a" by simp
-  { fix v assume "?sa = C v" hence ?case using sa by simp }
+  { fix v assume "?sa = C v" then have ?case using sa by simp }
   moreover {
     assume "\<not> (\<exists>v. ?sa = C v)"
-    hence ?case using sa by (cases ?sa) (simp_all add: Let_def)
+    then have ?case using sa by (cases ?sa) (simp_all add: Let_def)
   }
   ultimately show ?case by blast
 next
   case (10 a)
   let ?sa = "simpnum a"
   from simpnum_ci have sa: "Inum bs ?sa = Inum bs a" by simp
-  { fix v assume "?sa = C v" hence ?case using sa by simp }
+  { fix v assume "?sa = C v" then have ?case using sa by simp }
   moreover {
     assume "\<not> (\<exists>v. ?sa = C v)"
-    hence ?case using sa by (cases ?sa) (simp_all add: Let_def)
+    then have ?case using sa by (cases ?sa) (simp_all add: Let_def)
   }
   ultimately show ?case by blast
 next
   case (11 a)
   let ?sa = "simpnum a"
   from simpnum_ci have sa: "Inum bs ?sa = Inum bs a" by simp
-  { fix v assume "?sa = C v" hence ?case using sa by simp }
+  { fix v assume "?sa = C v" then have ?case using sa by simp }
   moreover {
     assume "\<not> (\<exists>v. ?sa = C v)"
-    hence ?case using sa by (cases ?sa) (simp_all add: Let_def)
+    then have ?case using sa by (cases ?sa) (simp_all add: Let_def)
   }
   ultimately show ?case by blast
 next
   case (12 i a)
   let ?sa = "simpnum a"
   from simpnum_ci have sa: "Inum bs ?sa = Inum bs a" by simp
-  { assume "i=0" hence ?case using "12.hyps" by (simp add: dvd_def Let_def) }
+  { assume "i=0" then have ?case using "12.hyps" by (simp add: dvd_def Let_def) }
   moreover
   { assume i1: "abs i = 1"
     from one_dvd[of "Inum bs a"] uminus_dvd_conv[where d="1" and t="Inum bs a"]
@@ -697,20 +703,20 @@
   moreover
   { assume inz: "i\<noteq>0" and cond: "abs i \<noteq> 1"
     { fix v assume "?sa = C v"
-      hence ?case using sa[symmetric] inz cond
+      then have ?case using sa[symmetric] inz cond
         by (cases "abs i = 1") auto }
     moreover {
       assume "\<not> (\<exists>v. ?sa = C v)"
-      hence "simpfm (Dvd i a) = Dvd i ?sa" using inz cond
+      then have "simpfm (Dvd i a) = Dvd i ?sa" using inz cond
         by (cases ?sa) (auto simp add: Let_def)
-      hence ?case using sa by simp }
+      then have ?case using sa by simp }
     ultimately have ?case by blast }
   ultimately show ?case by blast
 next
   case (13 i a)
   let ?sa = "simpnum a" from simpnum_ci
   have sa: "Inum bs ?sa = Inum bs a" by simp
-  { assume "i=0" hence ?case using "13.hyps" by (simp add: dvd_def Let_def) }
+  { assume "i=0" then have ?case using "13.hyps" by (simp add: dvd_def Let_def) }
   moreover
   { assume i1: "abs i = 1"
     from one_dvd[of "Inum bs a"] uminus_dvd_conv[where d="1" and t="Inum bs a"]
@@ -722,50 +728,50 @@
   moreover
   { assume inz: "i\<noteq>0" and cond: "abs i \<noteq> 1"
     { fix v assume "?sa = C v"
-      hence ?case using sa[symmetric] inz cond
+      then have ?case using sa[symmetric] inz cond
         by (cases "abs i = 1") auto }
     moreover {
       assume "\<not> (\<exists>v. ?sa = C v)"
-      hence "simpfm (NDvd i a) = NDvd i ?sa" using inz cond
+      then have "simpfm (NDvd i a) = NDvd i ?sa" using inz cond
         by (cases ?sa) (auto simp add: Let_def)
-      hence ?case using sa by simp }
+      then have ?case using sa by simp }
     ultimately have ?case by blast }
   ultimately show ?case by blast
 qed (simp_all add: conj disj imp iff not)
 
 lemma simpfm_bound0: "bound0 p \<Longrightarrow> bound0 (simpfm p)"
 proof (induct p rule: simpfm.induct)
-  case (6 a) hence nb: "numbound0 a" by simp
-  hence "numbound0 (simpnum a)" by (simp only: simpnum_numbound0[OF nb])
-  thus ?case by (cases "simpnum a") (auto simp add: Let_def)
+  case (6 a) then have nb: "numbound0 a" by simp
+  then have "numbound0 (simpnum a)" by (simp only: simpnum_numbound0[OF nb])
+  then show ?case by (cases "simpnum a") (auto simp add: Let_def)
 next
-  case (7 a) hence nb: "numbound0 a" by simp
-  hence "numbound0 (simpnum a)" by (simp only: simpnum_numbound0[OF nb])
-  thus ?case by (cases "simpnum a") (auto simp add: Let_def)
+  case (7 a) then have nb: "numbound0 a" by simp
+  then have "numbound0 (simpnum a)" by (simp only: simpnum_numbound0[OF nb])
+  then show ?case by (cases "simpnum a") (auto simp add: Let_def)
 next
-  case (8 a) hence nb: "numbound0 a" by simp
-  hence "numbound0 (simpnum a)" by (simp only: simpnum_numbound0[OF nb])
-  thus ?case by (cases "simpnum a") (auto simp add: Let_def)
+  case (8 a) then have nb: "numbound0 a" by simp
+  then have "numbound0 (simpnum a)" by (simp only: simpnum_numbound0[OF nb])
+  then show ?case by (cases "simpnum a") (auto simp add: Let_def)
 next
-  case (9 a) hence nb: "numbound0 a" by simp
-  hence "numbound0 (simpnum a)" by (simp only: simpnum_numbound0[OF nb])
-  thus ?case by (cases "simpnum a") (auto simp add: Let_def)
+  case (9 a) then have nb: "numbound0 a" by simp
+  then have "numbound0 (simpnum a)" by (simp only: simpnum_numbound0[OF nb])
+  then show ?case by (cases "simpnum a") (auto simp add: Let_def)
 next
-  case (10 a) hence nb: "numbound0 a" by simp
-  hence "numbound0 (simpnum a)" by (simp only: simpnum_numbound0[OF nb])
-  thus ?case by (cases "simpnum a") (auto simp add: Let_def)
+  case (10 a) then have nb: "numbound0 a" by simp
+  then have "numbound0 (simpnum a)" by (simp only: simpnum_numbound0[OF nb])
+  then show ?case by (cases "simpnum a") (auto simp add: Let_def)
 next
-  case (11 a) hence nb: "numbound0 a" by simp
-  hence "numbound0 (simpnum a)" by (simp only: simpnum_numbound0[OF nb])
-  thus ?case by (cases "simpnum a") (auto simp add: Let_def)
+  case (11 a) then have nb: "numbound0 a" by simp
+  then have "numbound0 (simpnum a)" by (simp only: simpnum_numbound0[OF nb])
+  then show ?case by (cases "simpnum a") (auto simp add: Let_def)
 next
-  case (12 i a) hence nb: "numbound0 a" by simp
-  hence "numbound0 (simpnum a)" by (simp only: simpnum_numbound0[OF nb])
-  thus ?case by (cases "simpnum a") (auto simp add: Let_def)
+  case (12 i a) then have nb: "numbound0 a" by simp
+  then have "numbound0 (simpnum a)" by (simp only: simpnum_numbound0[OF nb])
+  then show ?case by (cases "simpnum a") (auto simp add: Let_def)
 next
-  case (13 i a) hence nb: "numbound0 a" by simp
-  hence "numbound0 (simpnum a)" by (simp only: simpnum_numbound0[OF nb])
-  thus ?case by (cases "simpnum a") (auto simp add: Let_def)
+  case (13 i a) then have nb: "numbound0 a" by simp
+  then have "numbound0 (simpnum a)" by (simp only: simpnum_numbound0[OF nb])
+  then show ?case by (cases "simpnum a") (auto simp add: Let_def)
 qed (auto simp add: disj_def imp_def iff_def conj_def not_bn)
 
 lemma simpfm_qf: "qfree p \<Longrightarrow> qfree (simpfm p)"
@@ -787,8 +793,8 @@
 termination by (relation "measure fmsize") auto
 
 lemma qelim_ci:
-  assumes qe_inv: "\<forall>bs p. qfree p \<longrightarrow> qfree (qe p) \<and> (Ifm bbs bs (qe p) = Ifm bbs bs (E p))"
-  shows "\<And>bs. qfree (qelim p qe) \<and> (Ifm bbs bs (qelim p qe) = Ifm bbs bs p)"
+  assumes qe_inv: "\<forall>bs p. qfree p \<longrightarrow> qfree (qe p) \<and> Ifm bbs bs (qe p) = Ifm bbs bs (E p)"
+  shows "\<And>bs. qfree (qelim p qe) \<and> Ifm bbs bs (qelim p qe) = Ifm bbs bs p"
   using qe_inv DJ_qe[OF qe_inv]
   by(induct p rule: qelim.induct)
   (auto simp add: not disj conj iff imp not_qf disj_qf conj_qf imp_qf iff_qf
@@ -798,19 +804,23 @@
 
 fun zsplit0 :: "num \<Rightarrow> int \<times> num"  -- {* splits the bounded from the unbounded part *}
 where
-  "zsplit0 (C c) = (0,C c)"
-| "zsplit0 (Bound n) = (if n=0 then (1, C 0) else (0,Bound n))"
+  "zsplit0 (C c) = (0, C c)"
+| "zsplit0 (Bound n) = (if n = 0 then (1, C 0) else (0, Bound n))"
 | "zsplit0 (CN n i a) =
-    (let (i',a') =  zsplit0 a
-     in if n=0 then (i+i', a') else (i',CN n i a'))"
-| "zsplit0 (Neg a) = (let (i',a') =  zsplit0 a in (-i', Neg a'))"
-| "zsplit0 (Add a b) = (let (ia,a') =  zsplit0 a ;
-                          (ib,b') =  zsplit0 b
-                          in (ia+ib, Add a' b'))"
-| "zsplit0 (Sub a b) = (let (ia,a') =  zsplit0 a ;
-                          (ib,b') =  zsplit0 b
-                          in (ia-ib, Sub a' b'))"
-| "zsplit0 (Mul i a) = (let (i',a') =  zsplit0 a in (i*i', Mul i a'))"
+    (let (i', a') =  zsplit0 a
+     in if n = 0 then (i + i', a') else (i', CN n i a'))"
+| "zsplit0 (Neg a) = (let (i', a') = zsplit0 a in (-i', Neg a'))"
+| "zsplit0 (Add a b) =
+    (let
+      (ia, a') = zsplit0 a;
+      (ib, b') = zsplit0 b
+     in (ia + ib, Add a' b'))"
+| "zsplit0 (Sub a b) =
+    (let
+      (ia, a') = zsplit0 a;
+      (ib, b') = zsplit0 b
+     in (ia - ib, Sub a' b'))"
+| "zsplit0 (Mul i a) = (let (i', a') = zsplit0 a in (i*i', Mul i a'))"
 
 lemma zsplit0_I:
   shows "\<And>n a. zsplit0 t = (n,a) \<Longrightarrow> (Inum ((x::int) #bs) (CN 0 n a) = Inum (x #bs) t) \<and> numbound0 a"
@@ -925,19 +935,17 @@
 
 consts iszlfm :: "fm \<Rightarrow> bool"  -- {* Linearity test for fm *}
 recdef iszlfm "measure size"
-  "iszlfm (And p q) = (iszlfm p \<and> iszlfm q)"
-  "iszlfm (Or p q) = (iszlfm p \<and> iszlfm q)"
-  "iszlfm (Eq  (CN 0 c e)) = (c>0 \<and> numbound0 e)"
-  "iszlfm (NEq (CN 0 c e)) = (c>0 \<and> numbound0 e)"
-  "iszlfm (Lt  (CN 0 c e)) = (c>0 \<and> numbound0 e)"
-  "iszlfm (Le  (CN 0 c e)) = (c>0 \<and> numbound0 e)"
-  "iszlfm (Gt  (CN 0 c e)) = (c>0 \<and> numbound0 e)"
-  "iszlfm (Ge  (CN 0 c e)) = ( c>0 \<and> numbound0 e)"
-  "iszlfm (Dvd i (CN 0 c e)) =
-                 (c>0 \<and> i>0 \<and> numbound0 e)"
-  "iszlfm (NDvd i (CN 0 c e))=
-                 (c>0 \<and> i>0 \<and> numbound0 e)"
-  "iszlfm p = (isatom p \<and> (bound0 p))"
+  "iszlfm (And p q) \<longleftrightarrow> iszlfm p \<and> iszlfm q"
+  "iszlfm (Or p q) \<longleftrightarrow> iszlfm p \<and> iszlfm q"
+  "iszlfm (Eq  (CN 0 c e)) \<longleftrightarrow> c > 0 \<and> numbound0 e"
+  "iszlfm (NEq (CN 0 c e)) \<longleftrightarrow> c > 0 \<and> numbound0 e"
+  "iszlfm (Lt  (CN 0 c e)) \<longleftrightarrow> c > 0 \<and> numbound0 e"
+  "iszlfm (Le  (CN 0 c e)) \<longleftrightarrow> c > 0 \<and> numbound0 e"
+  "iszlfm (Gt  (CN 0 c e)) \<longleftrightarrow> c > 0 \<and> numbound0 e"
+  "iszlfm (Ge  (CN 0 c e)) \<longleftrightarrow> c > 0 \<and> numbound0 e"
+  "iszlfm (Dvd i (CN 0 c e)) \<longleftrightarrow> c > 0 \<and> i > 0 \<and> numbound0 e"
+  "iszlfm (NDvd i (CN 0 c e)) \<longleftrightarrow> c > 0 \<and> i > 0 \<and> numbound0 e"
+  "iszlfm p \<longleftrightarrow> isatom p \<and> bound0 p"
 
 lemma zlin_qfree: "iszlfm p \<Longrightarrow> qfree p"
   by (induct p rule: iszlfm.induct) auto
@@ -1264,7 +1272,7 @@
 qed simp_all
 
 lemma \<delta>:
-  assumes lin:"iszlfm p"
+  assumes lin: "iszlfm p"
   shows "d_\<delta> p (\<delta> p) \<and> \<delta> p >0"
   using lin
 proof (induct p rule: iszlfm.induct)
@@ -1396,11 +1404,11 @@
 proof (induct p rule: minusinf.induct)
   case (1 p q)
   then show ?case
-    by auto (rule_tac x="min z za" in exI,simp)
+    by auto (rule_tac x="min z za" in exI, simp)
 next
   case (2 p q)
   then show ?case
-    by auto (rule_tac x="min z za" in exI,simp)
+    by auto (rule_tac x="min z za" in exI, simp)
 next
   case (3 c e)
   then have c1: "c = 1" and nb: "numbound0 e"
@@ -1425,9 +1433,9 @@
     with numbound0_I[OF nb, where bs="bs" and b="a" and b'="x"]
     show "False" by simp
   qed
-  thus ?case by auto
+  then show ?case by auto
 next
-  case (5 c e) hence c1: "c=1" and nb: "numbound0 e" by simp_all
+  case (5 c e) then have c1: "c=1" and nb: "numbound0 e" by simp_all
   fix a
   from 5 have "\<forall>x<(- Inum (a#bs) e). c*x + Inum (x#bs) e < 0"
   proof(clarsimp)
@@ -1435,9 +1443,9 @@
     with numbound0_I[OF nb, where bs="bs" and b="a" and b'="x"]
     show "x + Inum (x#bs) e < 0" by simp
   qed
-  thus ?case by auto
+  then show ?case by auto
 next
-  case (6 c e) hence c1: "c=1" and nb: "numbound0 e" by simp_all
+  case (6 c e) then have c1: "c=1" and nb: "numbound0 e" by simp_all
   fix a
   from 6 have "\<forall>x<(- Inum (a#bs) e). c*x + Inum (x#bs) e \<le> 0"
   proof(clarsimp)
@@ -1445,9 +1453,9 @@
     with numbound0_I[OF nb, where bs="bs" and b="a" and b'="x"]
     show "x + Inum (x#bs) e \<le> 0" by simp
   qed
-  thus ?case by auto
+  then show ?case by auto
 next
-  case (7 c e) hence c1: "c=1" and nb: "numbound0 e" by simp_all
+  case (7 c e) then have c1: "c=1" and nb: "numbound0 e" by simp_all
   fix a
   from 7 have "\<forall>x<(- Inum (a#bs) e). \<not> (c*x + Inum (x#bs) e > 0)"
   proof(clarsimp)
@@ -1455,9 +1463,9 @@
     with numbound0_I[OF nb, where bs="bs" and b="a" and b'="x"]
     show "False" by simp
   qed
-  thus ?case by auto
+  then show ?case by auto
 next
-  case (8 c e) hence c1: "c=1" and nb: "numbound0 e" by simp_all
+  case (8 c e) then have c1: "c=1" and nb: "numbound0 e" by simp_all
   fix a
   from 8 have "\<forall>x<(- Inum (a#bs) e). \<not> (c*x + Inum (x#bs) e \<ge> 0)"
   proof(clarsimp)
@@ -1465,7 +1473,7 @@
     with numbound0_I[OF nb, where bs="bs" and b="a" and b'="x"]
     show "False" by simp
   qed
-  thus ?case by auto
+  then show ?case by auto
 qed auto
 
 lemma minusinf_repeats:
@@ -1474,56 +1482,56 @@
   using linp d
 proof (induct p rule: iszlfm.induct)
   case (9 i c e)
-  hence nbe: "numbound0 e" and id: "i dvd d" by simp_all
-  hence "\<exists>k. d=i*k" by (simp add: dvd_def)
+  then have nbe: "numbound0 e" and id: "i dvd d" by simp_all
+  then have "\<exists>k. d=i*k" by (simp add: dvd_def)
   then obtain "di" where di_def: "d=i*di" by blast
   show ?case
   proof (simp add: numbound0_I[OF nbe,where bs="bs" and b="x - k * d" and b'="x"] right_diff_distrib,
       rule iffI)
     assume "i dvd c * x - c*(k*d) + Inum (x # bs) e"
       (is "?ri dvd ?rc*?rx - ?rc*(?rk*?rd) + ?I x e" is "?ri dvd ?rt")
-    hence "\<exists>(l::int). ?rt = i * l" by (simp add: dvd_def)
-    hence "\<exists>(l::int). c*x+ ?I x e = i*l+c*(k * i*di)"
+    then have "\<exists>(l::int). ?rt = i * l" by (simp add: dvd_def)
+    then have "\<exists>(l::int). c*x+ ?I x e = i*l+c*(k * i*di)"
       by (simp add: algebra_simps di_def)
-    hence "\<exists>(l::int). c*x+ ?I x e = i*(l + c*k*di)"
+    then have "\<exists>(l::int). c*x+ ?I x e = i*(l + c*k*di)"
       by (simp add: algebra_simps)
-    hence "\<exists>(l::int). c*x+ ?I x e = i*l" by blast
-    thus "i dvd c*x + Inum (x # bs) e" by (simp add: dvd_def)
+    then have "\<exists>(l::int). c*x+ ?I x e = i*l" by blast
+    then show "i dvd c*x + Inum (x # bs) e" by (simp add: dvd_def)
   next
     assume "i dvd c*x + Inum (x # bs) e" (is "?ri dvd ?rc*?rx+?e")
-    hence "\<exists>(l::int). c*x+?e = i*l" by (simp add: dvd_def)
-    hence "\<exists>(l::int). c*x - c*(k*d) +?e = i*l - c*(k*d)" by simp
-    hence "\<exists>(l::int). c*x - c*(k*d) +?e = i*l - c*(k*i*di)" by (simp add: di_def)
-    hence "\<exists>(l::int). c*x - c*(k*d) +?e = i*((l - c*k*di))" by (simp add: algebra_simps)
-    hence "\<exists>(l::int). c*x - c * (k*d) +?e = i*l" by blast
-    thus "i dvd c*x - c*(k*d) + Inum (x # bs) e" by (simp add: dvd_def)
+    then have "\<exists>(l::int). c*x+?e = i*l" by (simp add: dvd_def)
+    then have "\<exists>(l::int). c*x - c*(k*d) +?e = i*l - c*(k*d)" by simp
+    then have "\<exists>(l::int). c*x - c*(k*d) +?e = i*l - c*(k*i*di)" by (simp add: di_def)
+    then have "\<exists>(l::int). c*x - c*(k*d) +?e = i*((l - c*k*di))" by (simp add: algebra_simps)
+    then have "\<exists>(l::int). c*x - c * (k*d) +?e = i*l" by blast
+    then show "i dvd c*x - c*(k*d) + Inum (x # bs) e" by (simp add: dvd_def)
   qed
 next
   case (10 i c e)
-  hence nbe: "numbound0 e"  and id: "i dvd d" by simp_all
-  hence "\<exists>k. d=i*k" by (simp add: dvd_def)
+  then have nbe: "numbound0 e"  and id: "i dvd d" by simp_all
+  then have "\<exists>k. d=i*k" by (simp add: dvd_def)
   then obtain "di" where di_def: "d=i*di" by blast
   show ?case
   proof(simp add: numbound0_I[OF nbe,where bs="bs" and b="x - k * d" and b'="x"] right_diff_distrib, rule iffI)
     assume "i dvd c * x - c*(k*d) + Inum (x # bs) e"
       (is "?ri dvd ?rc*?rx - ?rc*(?rk*?rd) + ?I x e" is "?ri dvd ?rt")
-    hence "\<exists>(l::int). ?rt = i * l" by (simp add: dvd_def)
-    hence "\<exists>(l::int). c*x+ ?I x e = i*l+c*(k * i*di)"
+    then have "\<exists>(l::int). ?rt = i * l" by (simp add: dvd_def)
+    then have "\<exists>(l::int). c*x+ ?I x e = i*l+c*(k * i*di)"
       by (simp add: algebra_simps di_def)
-    hence "\<exists>(l::int). c*x+ ?I x e = i*(l + c*k*di)"
+    then have "\<exists>(l::int). c*x+ ?I x e = i*(l + c*k*di)"
       by (simp add: algebra_simps)
-    hence "\<exists>(l::int). c*x+ ?I x e = i*l" by blast
-    thus "i dvd c*x + Inum (x # bs) e" by (simp add: dvd_def)
+    then have "\<exists>(l::int). c*x+ ?I x e = i*l" by blast
+    then show "i dvd c*x + Inum (x # bs) e" by (simp add: dvd_def)
   next
     assume
       "i dvd c*x + Inum (x # bs) e" (is "?ri dvd ?rc*?rx+?e")
-    hence "\<exists>(l::int). c*x+?e = i*l" by (simp add: dvd_def)
-    hence "\<exists>(l::int). c*x - c*(k*d) +?e = i*l - c*(k*d)" by simp
-    hence "\<exists>(l::int). c*x - c*(k*d) +?e = i*l - c*(k*i*di)" by (simp add: di_def)
-    hence "\<exists>(l::int). c*x - c*(k*d) +?e = i*((l - c*k*di))" by (simp add: algebra_simps)
-    hence "\<exists>(l::int). c*x - c * (k*d) +?e = i*l"
+    then have "\<exists>(l::int). c*x+?e = i*l" by (simp add: dvd_def)
+    then have "\<exists>(l::int). c*x - c*(k*d) +?e = i*l - c*(k*d)" by simp
+    then have "\<exists>(l::int). c*x - c*(k*d) +?e = i*l - c*(k*i*di)" by (simp add: di_def)
+    then have "\<exists>(l::int). c*x - c*(k*d) +?e = i*((l - c*k*di))" by (simp add: algebra_simps)
+    then have "\<exists>(l::int). c*x - c * (k*d) +?e = i*l"
       by blast
-    thus "i dvd c*x - c*(k*d) + Inum (x # bs) e" by (simp add: dvd_def)
+    then show "i dvd c*x - c*(k*d) + Inum (x # bs) e" by (simp add: dvd_def)
   qed
 qed (auto simp add: gr0_conv_Suc numbound0_I[where bs="bs" and b="x - k*d" and b'="x"])
 
@@ -1538,7 +1546,7 @@
   using lp
 proof (induct p rule: iszlfm.induct)
   case (9 j c e)
-  hence nb: "numbound0 e" by simp
+  then have nb: "numbound0 e" by simp
   have "Ifm bbs (x#bs) (mirror (Dvd j (CN 0 c e))) = (j dvd c*x - Inum (x#bs) e)"
     (is "_ = (j dvd c*x - ?e)") by simp
   also have "\<dots> = (j dvd (- (c*x - ?e)))"
@@ -1550,7 +1558,7 @@
     using numbound0_I[OF nb, where bs="bs" and b="x" and b'="- x"] by simp
   finally show ?case .
 next
-  case (10 j c e) hence nb: "numbound0 e" by simp
+  case (10 j c e) then have nb: "numbound0 e" by simp
   have "Ifm bbs (x#bs) (mirror (Dvd j (CN 0 c e))) = (j dvd c*x - Inum (x#bs) e)"
     (is "_ = (j dvd c*x - ?e)") by simp
   also have "\<dots> = (j dvd (- (c*x - ?e)))"
@@ -1613,7 +1621,7 @@
   using linp d
 proof (induct p rule: iszlfm.induct)
   case (5 c e)
-  hence cp: "c>0" and be: "numbound0 e" and d': "c dvd l" by simp_all
+  then have cp: "c>0" and be: "numbound0 e" and d': "c dvd l" by simp_all
   from lp cp have clel: "c\<le>l" by (simp add: zdvd_imp_le [OF d' lp])
   from cp have cnz: "c \<noteq> 0" by simp
   have "c div c\<le> l div c"
@@ -1622,9 +1630,9 @@
     by (simp add: div_self[OF cnz])
   have "c * (l div c) = c* (l div c) + l mod c" using d' dvd_eq_mod_eq_0[of "c" "l"]
     by simp
-  hence cl:"c * (l div c) =l" using zmod_zdiv_equality[where a="l" and b="c", symmetric]
+  then have cl:"c * (l div c) =l" using zmod_zdiv_equality[where a="l" and b="c", symmetric]
     by simp
-  hence "(l*x + (l div c) * Inum (x # bs) e < 0) =
+  then have "(l*x + (l div c) * Inum (x # bs) e < 0) =
       ((c * (l div c)) * x + (l div c) * Inum (x # bs) e < 0)"
     by simp
   also have "\<dots> = ((l div c) * (c*x + Inum (x # bs) e) < (l div c) * 0)"
@@ -1635,7 +1643,7 @@
     using numbound0_I[OF be,where b="l*x" and b'="x" and bs="bs"] be by simp
 next
   case (6 c e)
-  hence cp: "c>0" and be: "numbound0 e" and d': "c dvd l" by simp_all
+  then have cp: "c>0" and be: "numbound0 e" and d': "c dvd l" by simp_all
   from lp cp have clel: "c\<le>l" by (simp add: zdvd_imp_le [OF d' lp])
   from cp have cnz: "c \<noteq> 0" by simp
   have "c div c\<le> l div c"
@@ -1644,9 +1652,9 @@
     by (simp add: div_self[OF cnz])
   have "c * (l div c) = c* (l div c) + l mod c" using d' dvd_eq_mod_eq_0[of "c" "l"]
     by simp
-  hence cl:"c * (l div c) =l" using zmod_zdiv_equality[where a="l" and b="c", symmetric]
+  then have cl:"c * (l div c) =l" using zmod_zdiv_equality[where a="l" and b="c", symmetric]
     by simp
-  hence "(l*x + (l div c) * Inum (x# bs) e \<le> 0) =
+  then have "(l*x + (l div c) * Inum (x# bs) e \<le> 0) =
       ((c * (l div c)) * x + (l div c) * Inum (x # bs) e \<le> 0)" by simp
   also have "\<dots> = ((l div c) * (c * x + Inum (x # bs) e) \<le> ((l div c)) * 0)"
     by (simp add: algebra_simps)
@@ -1656,7 +1664,7 @@
     using numbound0_I[OF be,where b="l*x" and b'="x" and bs="bs"] be by simp
 next
   case (7 c e)
-  hence cp: "c>0" and be: "numbound0 e" and d': "c dvd l" by simp_all
+  then have cp: "c>0" and be: "numbound0 e" and d': "c dvd l" by simp_all
   from lp cp have clel: "c\<le>l" by (simp add: zdvd_imp_le [OF d' lp])
   from cp have cnz: "c \<noteq> 0" by simp
   have "c div c\<le> l div c"
@@ -1665,9 +1673,9 @@
     by (simp add: div_self[OF cnz])
   have "c * (l div c) = c* (l div c) + l mod c"
     using d' dvd_eq_mod_eq_0[of "c" "l"] by simp
-  hence cl:"c * (l div c) =l" using zmod_zdiv_equality[where a="l" and b="c", symmetric]
+  then have cl:"c * (l div c) =l" using zmod_zdiv_equality[where a="l" and b="c", symmetric]
     by simp
-  hence "(l*x + (l div c)* Inum (x # bs) e > 0) =
+  then have "(l*x + (l div c)* Inum (x # bs) e > 0) =
       ((c * (l div c)) * x + (l div c) * Inum (x # bs) e > 0)" by simp
   also have "\<dots> = ((l div c) * (c * x + Inum (x # bs) e) > ((l div c)) * 0)"
     by (simp add: algebra_simps)
@@ -1677,7 +1685,7 @@
     using numbound0_I[OF be,where b="(l * x)" and b'="x" and bs="bs"] be by simp
 next
   case (8 c e)
-  hence cp: "c>0" and be: "numbound0 e" and d': "c dvd l" by simp_all
+  then have cp: "c>0" and be: "numbound0 e" and d': "c dvd l" by simp_all
   from lp cp have clel: "c\<le>l" by (simp add: zdvd_imp_le [OF d' lp])
   from cp have cnz: "c \<noteq> 0" by simp
   have "c div c\<le> l div c"
@@ -1686,9 +1694,9 @@
     by (simp add: div_self[OF cnz])
   have "c * (l div c) = c* (l div c) + l mod c" using d' dvd_eq_mod_eq_0[of "c" "l"]
     by simp
-  hence cl:"c * (l div c) =l" using zmod_zdiv_equality[where a="l" and b="c", symmetric]
+  then have cl:"c * (l div c) =l" using zmod_zdiv_equality[where a="l" and b="c", symmetric]
     by simp
-  hence "(l*x + (l div c)* Inum (x # bs) e \<ge> 0) =
+  then have "(l*x + (l div c)* Inum (x # bs) e \<ge> 0) =
       ((c*(l div c))*x + (l div c)* Inum (x # bs) e \<ge> 0)" by simp
   also have "\<dots> = ((l div c)*(c*x + Inum (x # bs) e) \<ge> ((l div c)) * 0)"
     by (simp add: algebra_simps)
@@ -1698,7 +1706,7 @@
     using be numbound0_I[OF be,where b="l*x" and b'="x" and bs="bs"] by simp
 next
   case (3 c e)
-  hence cp: "c>0" and be: "numbound0 e" and d': "c dvd l" by simp_all
+  then have cp: "c>0" and be: "numbound0 e" and d': "c dvd l" by simp_all
   from lp cp have clel: "c\<le>l" by (simp add: zdvd_imp_le [OF d' lp])
   from cp have cnz: "c \<noteq> 0" by simp
   have "c div c\<le> l div c"
@@ -1707,9 +1715,9 @@
     by (simp add: div_self[OF cnz])
   have "c * (l div c) = c* (l div c) + l mod c" using d' dvd_eq_mod_eq_0[of "c" "l"]
     by simp
-  hence cl:"c * (l div c) =l" using zmod_zdiv_equality[where a="l" and b="c", symmetric]
+  then have cl:"c * (l div c) =l" using zmod_zdiv_equality[where a="l" and b="c", symmetric]
     by simp
-  hence "(l * x + (l div c) * Inum (x # bs) e = 0) =
+  then have "(l * x + (l div c) * Inum (x # bs) e = 0) =
       ((c * (l div c)) * x + (l div c) * Inum (x # bs) e = 0)" by simp
   also have "\<dots> = ((l div c) * (c * x + Inum (x # bs) e) = ((l div c)) * 0)"
     by (simp add: algebra_simps)
@@ -1719,7 +1727,7 @@
     using numbound0_I[OF be,where b="(l * x)" and b'="x" and bs="bs"] be by simp
 next
   case (4 c e)
-  hence cp: "c>0" and be: "numbound0 e" and d': "c dvd l" by simp_all
+  then have cp: "c>0" and be: "numbound0 e" and d': "c dvd l" by simp_all
   from lp cp have clel: "c\<le>l" by (simp add: zdvd_imp_le [OF d' lp])
   from cp have cnz: "c \<noteq> 0" by simp
   have "c div c\<le> l div c"
@@ -1728,9 +1736,9 @@
     by (simp add: div_self[OF cnz])
   have "c * (l div c) = c* (l div c) + l mod c" using d' dvd_eq_mod_eq_0[of "c" "l"]
     by simp
-  hence cl:"c * (l div c) =l" using zmod_zdiv_equality[where a="l" and b="c", symmetric]
+  then have cl:"c * (l div c) =l" using zmod_zdiv_equality[where a="l" and b="c", symmetric]
     by simp
-  hence "(l * x + (l div c) * Inum (x # bs) e \<noteq> 0) =
+  then have "(l * x + (l div c) * Inum (x # bs) e \<noteq> 0) =
       ((c * (l div c)) * x + (l div c) * Inum (x # bs) e \<noteq> 0)" by simp
   also have "\<dots> = ((l div c) * (c * x + Inum (x # bs) e) \<noteq> ((l div c)) * 0)"
     by (simp add: algebra_simps)
@@ -1740,7 +1748,7 @@
     using numbound0_I[OF be,where b="(l * x)" and b'="x" and bs="bs"] be by simp
 next
   case (9 j c e)
-  hence cp: "c>0" and be: "numbound0 e" and jp: "j > 0" and d': "c dvd l" by simp_all
+  then have cp: "c>0" and be: "numbound0 e" and jp: "j > 0" and d': "c dvd l" by simp_all
   from lp cp have clel: "c\<le>l" by (simp add: zdvd_imp_le [OF d' lp])
   from cp have cnz: "c \<noteq> 0" by simp
   have "c div c\<le> l div c"
@@ -1749,9 +1757,9 @@
     by (simp add: div_self[OF cnz])
   have "c * (l div c) = c* (l div c) + l mod c" using d' dvd_eq_mod_eq_0[of "c" "l"]
     by simp
-  hence cl:"c * (l div c) =l" using zmod_zdiv_equality[where a="l" and b="c", symmetric]
+  then have cl:"c * (l div c) =l" using zmod_zdiv_equality[where a="l" and b="c", symmetric]
     by simp
-  hence "(\<exists>(k::int). l * x + (l div c) * Inum (x # bs) e = ((l div c) * j) * k) =
+  then have "(\<exists>(k::int). l * x + (l div c) * Inum (x # bs) e = ((l div c) * j) * k) =
     (\<exists>(k::int). (c * (l div c)) * x + (l div c) * Inum (x # bs) e = ((l div c) * j) * k)" by simp
   also have "\<dots> = (\<exists>(k::int). (l div c) * (c * x + Inum (x # bs) e - j * k) = (l div c)*0)"
     by (simp add: algebra_simps)
@@ -1764,17 +1772,20 @@
     by (simp add: dvd_def)
 next
   case (10 j c e)
-  hence cp: "c>0" and be: "numbound0 e" and jp: "j > 0" and d': "c dvd l" by simp_all
+  then have cp: "c>0" and be: "numbound0 e" and jp: "j > 0" and d': "c dvd l" by simp_all
   from lp cp have clel: "c\<le>l" by (simp add: zdvd_imp_le [OF d' lp])
   from cp have cnz: "c \<noteq> 0" by simp
   have "c div c\<le> l div c"
     by (simp add: zdiv_mono1[OF clel cp])
   then have ldcp:"0 < l div c"
     by (simp add: div_self[OF cnz])
-  have "c * (l div c) = c* (l div c) + l mod c" using d' dvd_eq_mod_eq_0[of "c" "l"] by simp
-  hence cl:"c * (l div c) =l" using zmod_zdiv_equality[where a="l" and b="c", symmetric]
+  have "c * (l div c) = c* (l div c) + l mod c"
+    using d' dvd_eq_mod_eq_0[of "c" "l"] by simp
+  then have cl:"c * (l div c) =l"
+    using zmod_zdiv_equality[where a="l" and b="c", symmetric] by simp
+  then have "(\<exists>(k::int). l * x + (l div c) * Inum (x # bs) e =
+      ((l div c) * j) * k) = (\<exists>(k::int). (c * (l div c)) * x + (l div c) * Inum (x # bs) e = ((l div c) * j) * k)"
     by simp
-  hence "(\<exists>(k::int). l * x + (l div c) * Inum (x # bs) e = ((l div c) * j) * k) = (\<exists>(k::int). (c * (l div c)) * x + (l div c) * Inum (x # bs) e = ((l div c) * j) * k)"  by simp
   also have "\<dots> = (\<exists>(k::int). (l div c) * (c * x + Inum (x # bs) e - j * k) = (l div c)*0)" by (simp add: algebra_simps)
   also fix k have "\<dots> = (\<exists>(k::int). c * x + Inum (x # bs) e - j * k = 0)"
     using zero_le_mult_iff [where a="(l div c)" and b="c * x + Inum (x # bs) e - j * k"] ldcp by simp
@@ -1794,97 +1805,166 @@
 
 lemma \<beta>:
   assumes lp: "iszlfm p"
-  and u: "d_\<beta> p 1"
-  and d: "d_\<delta> p d"
-  and dp: "d > 0"
-  and nob: "\<not>(\<exists>(j::int) \<in> {1 .. d}. \<exists>b\<in> (Inum (a#bs)) ` set(\<beta> p). x = b + j)"
-  and p: "Ifm bbs (x#bs) p" (is "?P x")
+    and u: "d_\<beta> p 1"
+    and d: "d_\<delta> p d"
+    and dp: "d > 0"
+    and nob: "\<not>(\<exists>(j::int) \<in> {1 .. d}. \<exists>b\<in> (Inum (a#bs)) ` set(\<beta> p). x = b + j)"
+    and p: "Ifm bbs (x#bs) p" (is "?P x")
   shows "?P (x - d)"
-using lp u d dp nob p
-proof(induct p rule: iszlfm.induct)
-  case (5 c e) hence c1: "c=1" and  bn:"numbound0 e" by simp_all
+  using lp u d dp nob p
+proof (induct p rule: iszlfm.induct)
+  case (5 c e)
+  then have c1: "c = 1" and  bn: "numbound0 e"
+    by simp_all
   with dp p c1 numbound0_I[OF bn,where b="(x-d)" and b'="x" and bs="bs"] 5
   show ?case by simp
 next
-  case (6 c e)  hence c1: "c=1" and  bn:"numbound0 e" by simp_all
+  case (6 c e)
+  then have c1: "c = 1" and  bn: "numbound0 e"
+    by simp_all
   with dp p c1 numbound0_I[OF bn,where b="(x-d)" and b'="x" and bs="bs"] 6
   show ?case by simp
 next
-  case (7 c e) hence p: "Ifm bbs (x #bs) (Gt (CN 0 c e))" and c1: "c=1" and bn:"numbound0 e" by simp_all
+  case (7 c e)
+  then have p: "Ifm bbs (x #bs) (Gt (CN 0 c e))" and c1: "c=1" and bn: "numbound0 e"
+    by simp_all
   let ?e = "Inum (x # bs) e"
-  {assume "(x-d) +?e > 0" hence ?case using c1
-    numbound0_I[OF bn,where b="(x-d)" and b'="x" and bs="bs"] by simp}
+  {
+    assume "(x-d) +?e > 0"
+    then have ?case
+      using c1 numbound0_I[OF bn,where b="(x-d)" and b'="x" and bs="bs"] by simp
+  }
   moreover
-  {assume H: "\<not> (x-d) + ?e > 0"
+  {
+    assume H: "\<not> (x-d) + ?e > 0"
     let ?v="Neg e"
     have vb: "?v \<in> set (\<beta> (Gt (CN 0 c e)))" by simp
     from 7(5)[simplified simp_thms Inum.simps \<beta>.simps set_simps bex_simps numbound0_I[OF bn,where b="a" and b'="x" and bs="bs"]]
-    have nob: "\<not> (\<exists>j\<in> {1 ..d}. x =  - ?e + j)" by auto
-    from H p have "x + ?e > 0 \<and> x + ?e \<le> d" by (simp add: c1)
-    hence "x + ?e \<ge> 1 \<and> x + ?e \<le> d"  by simp
-    hence "\<exists>(j::int) \<in> {1 .. d}. j = x + ?e" by simp
-    hence "\<exists>(j::int) \<in> {1 .. d}. x = (- ?e + j)"
+    have nob: "\<not> (\<exists>j\<in> {1 ..d}. x =  - ?e + j)"
+      by auto
+    from H p have "x + ?e > 0 \<and> x + ?e \<le> d"
+      by (simp add: c1)
+    then have "x + ?e \<ge> 1 \<and> x + ?e \<le> d"
+      by simp
+    then have "\<exists>(j::int) \<in> {1 .. d}. j = x + ?e"
+      by simp
+    then have "\<exists>(j::int) \<in> {1 .. d}. x = (- ?e + j)"
       by (simp add: algebra_simps)
-    with nob have ?case by auto}
-  ultimately show ?case by blast
+    with nob have ?case
+      by auto
+  }
+  ultimately show ?case
+    by blast
 next
-  case (8 c e) hence p: "Ifm bbs (x #bs) (Ge (CN 0 c e))" and c1: "c=1" and bn:"numbound0 e"
+  case (8 c e)
+  then have p: "Ifm bbs (x # bs) (Ge (CN 0 c e))" and c1: "c = 1" and bn: "numbound0 e"
     by simp_all
-    let ?e = "Inum (x # bs) e"
-    {assume "(x-d) +?e \<ge> 0" hence ?case using  c1
-      numbound0_I[OF bn,where b="(x-d)" and b'="x" and bs="bs"]
-        by simp}
-    moreover
-    {assume H: "\<not> (x-d) + ?e \<ge> 0"
-      let ?v="Sub (C -1) e"
-      have vb: "?v \<in> set (\<beta> (Ge (CN 0 c e)))" by simp
-      from 8(5)[simplified simp_thms Inum.simps \<beta>.simps set_simps bex_simps numbound0_I[OF bn,where b="a" and b'="x" and bs="bs"]]
-      have nob: "\<not> (\<exists>j\<in> {1 ..d}. x =  - ?e - 1 + j)" by auto
-      from H p have "x + ?e \<ge> 0 \<and> x + ?e < d" by (simp add: c1)
-      hence "x + ?e +1 \<ge> 1 \<and> x + ?e + 1 \<le> d"  by simp
-      hence "\<exists>(j::int) \<in> {1 .. d}. j = x + ?e + 1" by simp
-      hence "\<exists>(j::int) \<in> {1 .. d}. x= - ?e - 1 + j" by (simp add: algebra_simps)
-      with nob have ?case by simp }
-    ultimately show ?case by blast
+  let ?e = "Inum (x # bs) e"
+  {
+    assume "(x - d) + ?e \<ge> 0"
+    then have ?case
+      using c1 numbound0_I[OF bn,where b="(x-d)" and b'="x" and bs="bs"]
+      by simp
+  }
+  moreover
+  {
+    assume H: "\<not> (x - d) + ?e \<ge> 0"
+    let ?v = "Sub (C -1) e"
+    have vb: "?v \<in> set (\<beta> (Ge (CN 0 c e)))"
+      by simp
+    from 8(5)[simplified simp_thms Inum.simps \<beta>.simps set_simps bex_simps numbound0_I[OF bn,where b="a" and b'="x" and bs="bs"]]
+    have nob: "\<not> (\<exists>j\<in> {1 ..d}. x =  - ?e - 1 + j)"
+      by auto
+    from H p have "x + ?e \<ge> 0 \<and> x + ?e < d"
+      by (simp add: c1)
+    then have "x + ?e +1 \<ge> 1 \<and> x + ?e + 1 \<le> d"
+      by simp
+    then have "\<exists>(j::int) \<in> {1 .. d}. j = x + ?e + 1"
+      by simp
+    then have "\<exists>(j::int) \<in> {1 .. d}. x= - ?e - 1 + j"
+      by (simp add: algebra_simps)
+    with nob have ?case
+      by simp
+  }
+  ultimately show ?case
+    by blast
 next
-  case (3 c e) hence p: "Ifm bbs (x #bs) (Eq (CN 0 c e))" (is "?p x") and c1: "c=1" and bn:"numbound0 e" by simp_all
-    let ?e = "Inum (x # bs) e"
-    let ?v="(Sub (C -1) e)"
-    have vb: "?v \<in> set (\<beta> (Eq (CN 0 c e)))" by simp
-    from p have "x= - ?e" by (simp add: c1) with 3(5) show ?case using dp
-      by simp (erule ballE[where x="1"],
-        simp_all add:algebra_simps numbound0_I[OF bn,where b="x"and b'="a"and bs="bs"])
+  case (3 c e)
+  then
+  have p: "Ifm bbs (x #bs) (Eq (CN 0 c e))" (is "?p x")
+    and c1: "c=1"
+    and bn: "numbound0 e"
+    by simp_all
+  let ?e = "Inum (x # bs) e"
+  let ?v="(Sub (C -1) e)"
+  have vb: "?v \<in> set (\<beta> (Eq (CN 0 c e)))"
+    by simp
+  from p have "x= - ?e" by (simp add: c1) with 3(5) show ?case
+    using dp
+    by simp (erule ballE[where x="1"],
+      simp_all add:algebra_simps numbound0_I[OF bn,where b="x"and b'="a"and bs="bs"])
 next
-  case (4 c e)hence p: "Ifm bbs (x #bs) (NEq (CN 0 c e))" (is "?p x") and c1: "c=1" and bn:"numbound0 e" by simp_all
-    let ?e = "Inum (x # bs) e"
-    let ?v="Neg e"
-    have vb: "?v \<in> set (\<beta> (NEq (CN 0 c e)))" by simp
-    {assume "x - d + Inum (((x -d)) # bs) e \<noteq> 0"
-      hence ?case by (simp add: c1)}
-    moreover
-    {assume H: "x - d + Inum (((x -d)) # bs) e = 0"
-      hence "x = - Inum (((x -d)) # bs) e + d" by simp
-      hence "x = - Inum (a # bs) e + d"
-        by (simp add: numbound0_I[OF bn,where b="x - d"and b'="a"and bs="bs"])
-       with 4(5) have ?case using dp by simp}
-  ultimately show ?case by blast
+  case (4 c e)
+  then
+  have p: "Ifm bbs (x #bs) (NEq (CN 0 c e))" (is "?p x")
+    and c1: "c = 1"
+    and bn: "numbound0 e"
+    by simp_all
+  let ?e = "Inum (x # bs) e"
+  let ?v="Neg e"
+  have vb: "?v \<in> set (\<beta> (NEq (CN 0 c e)))" by simp
+  {
+    assume "x - d + Inum (((x -d)) # bs) e \<noteq> 0"
+    then have ?case by (simp add: c1)
+  }
+  moreover
+  {
+    assume H: "x - d + Inum (((x -d)) # bs) e = 0"
+    then have "x = - Inum (((x -d)) # bs) e + d"
+      by simp
+    then have "x = - Inum (a # bs) e + d"
+      by (simp add: numbound0_I[OF bn,where b="x - d"and b'="a"and bs="bs"])
+     with 4(5) have ?case
+      using dp by simp
+  }
+  ultimately show ?case
+    by blast
 next
-  case (9 j c e) hence p: "Ifm bbs (x #bs) (Dvd j (CN 0 c e))" (is "?p x") and c1: "c=1" and bn:"numbound0 e" by simp_all
-    let ?e = "Inum (x # bs) e"
-    from 9 have id: "j dvd d" by simp
-    from c1 have "?p x = (j dvd (x+ ?e))" by simp
-    also have "\<dots> = (j dvd x - d + ?e)"
-      using zdvd_period[OF id, where x="x" and c="-1" and t="?e"] by simp
-    finally show ?case
-      using numbound0_I[OF bn,where b="(x-d)" and b'="x" and bs="bs"] c1 p by simp
+  case (9 j c e)
+  then
+  have p: "Ifm bbs (x # bs) (Dvd j (CN 0 c e))" (is "?p x")
+    and c1: "c = 1"
+    and bn: "numbound0 e"
+    by simp_all
+  let ?e = "Inum (x # bs) e"
+  from 9 have id: "j dvd d"
+    by simp
+  from c1 have "?p x = (j dvd (x + ?e))"
+    by simp
+  also have "\<dots> = (j dvd x - d + ?e)"
+    using zdvd_period[OF id, where x="x" and c="-1" and t="?e"]
+    by simp
+  finally show ?case
+    using numbound0_I[OF bn,where b="(x-d)" and b'="x" and bs="bs"] c1 p
+    by simp
 next
-  case (10 j c e) hence p: "Ifm bbs (x #bs) (NDvd j (CN 0 c e))" (is "?p x") and c1: "c=1" and bn:"numbound0 e" by simp_all
-    let ?e = "Inum (x # bs) e"
-    from 10 have id: "j dvd d" by simp
-    from c1 have "?p x = (\<not> j dvd (x+ ?e))" by simp
-    also have "\<dots> = (\<not> j dvd x - d + ?e)"
-      using zdvd_period[OF id, where x="x" and c="-1" and t="?e"] by simp
-    finally show ?case using numbound0_I[OF bn,where b="(x-d)" and b'="x" and bs="bs"] c1 p by simp
+  case (10 j c e)
+  then
+  have p: "Ifm bbs (x #bs) (NDvd j (CN 0 c e))" (is "?p x")
+    and c1: "c = 1"
+    and bn: "numbound0 e"
+    by simp_all
+  let ?e = "Inum (x # bs) e"
+  from 10 have id: "j dvd d"
+    by simp
+  from c1 have "?p x = (\<not> j dvd (x + ?e))"
+    by simp
+  also have "\<dots> = (\<not> j dvd x - d + ?e)"
+    using zdvd_period[OF id, where x="x" and c="-1" and t="?e"]
+    by simp
+  finally show ?case
+    using numbound0_I[OF bn,where b="(x-d)" and b'="x" and bs="bs"] c1 p
+    by simp
 qed (auto simp add: numbound0_I[where bs="bs" and b="(x - d)" and b'="x"] gr0_conv_Suc)
 
 lemma \<beta>':
@@ -1892,67 +1972,75 @@
   and u: "d_\<beta> p 1"
   and d: "d_\<delta> p d"
   and dp: "d > 0"
-  shows "\<forall>x. \<not>(\<exists>(j::int) \<in> {1 .. d}. \<exists>b\<in> set(\<beta> p). Ifm bbs ((Inum (a#bs) b + j) #bs) p) \<longrightarrow> Ifm bbs (x#bs) p \<longrightarrow> Ifm bbs ((x - d)#bs) p" (is "\<forall>x. ?b \<longrightarrow> ?P x \<longrightarrow> ?P (x - d)")
-proof(clarify)
+  shows "\<forall>x. \<not> (\<exists>(j::int) \<in> {1 .. d}. \<exists>b\<in> set(\<beta> p). Ifm bbs ((Inum (a#bs) b + j) #bs) p) \<longrightarrow>
+    Ifm bbs (x#bs) p \<longrightarrow> Ifm bbs ((x - d)#bs) p" (is "\<forall>x. ?b \<longrightarrow> ?P x \<longrightarrow> ?P (x - d)")
+proof clarify
   fix x
-  assume nb:"?b" and px: "?P x"
-  hence nb2: "\<not>(\<exists>(j::int) \<in> {1 .. d}. \<exists>b\<in> (Inum (a#bs)) ` set(\<beta> p). x = b + j)"
+  assume nb: "?b"
+    and px: "?P x"
+  then have nb2: "\<not>(\<exists>(j::int) \<in> {1 .. d}. \<exists>b\<in> (Inum (a#bs)) ` set(\<beta> p). x = b + j)"
     by auto
   from  \<beta>[OF lp u d dp nb2 px] show "?P (x -d )" .
 qed
-lemma cpmi_eq: "0 < D \<Longrightarrow> (EX z::int. ALL x. x < z --> (P x = P1 x))
-==> ALL x.~(EX (j::int) : {1..D}. EX (b::int) : B. P(b+j)) --> P (x) --> P (x - D)
-==> (ALL (x::int). ALL (k::int). ((P1 x)= (P1 (x-k*D))))
-==> (EX (x::int). P(x)) = ((EX (j::int) : {1..D} . (P1(j))) | (EX (j::int) : {1..D}. EX (b::int) : B. P (b+j)))"
-apply(rule iffI)
-prefer 2
-apply(drule minusinfinity)
-apply assumption+
-apply(fastforce)
-apply clarsimp
-apply(subgoal_tac "!!k. 0<=k \<Longrightarrow> !x. P x \<longrightarrow> P (x - k*D)")
-apply(frule_tac x = x and z=z in decr_lemma)
-apply(subgoal_tac "P1(x - (\<bar>x - z\<bar> + 1) * D)")
-prefer 2
-apply(subgoal_tac "0 <= (\<bar>x - z\<bar> + 1)")
-prefer 2 apply arith
- apply fastforce
-apply(drule (1)  periodic_finite_ex)
-apply blast
-apply(blast dest:decr_mult_lemma)
-done
+
+lemma cpmi_eq:
+  "0 < D \<Longrightarrow> (\<exists>z::int. \<forall>x. x < z \<longrightarrow> P x = P1 x)
+    \<Longrightarrow> \<forall>x. \<not>(\<exists>(j::int) \<in> {1..D}. \<exists>(b::int) \<in> B. P (b + j)) \<longrightarrow> P x \<longrightarrow> P (x - D)
+    \<Longrightarrow> (\<forall>(x::int). \<forall>(k::int). P1 x = (P1 (x - k * D)))
+    \<Longrightarrow> (\<exists>(x::int). P x) = ((\<exists>(j::int) \<in> {1..D}. P1 j) \<or> (\<exists>(j::int) \<in> {1..D}. \<exists>(b::int) \<in> B. P (b + j)))"
+  apply(rule iffI)
+  prefer 2
+  apply(drule minusinfinity)
+  apply assumption+
+  apply(fastforce)
+  apply clarsimp
+  apply(subgoal_tac "!!k. 0<=k \<Longrightarrow> !x. P x \<longrightarrow> P (x - k*D)")
+  apply(frule_tac x = x and z=z in decr_lemma)
+  apply(subgoal_tac "P1(x - (\<bar>x - z\<bar> + 1) * D)")
+  prefer 2
+  apply(subgoal_tac "0 <= (\<bar>x - z\<bar> + 1)")
+  prefer 2 apply arith
+   apply fastforce
+  apply(drule (1)  periodic_finite_ex)
+  apply blast
+  apply(blast dest:decr_mult_lemma)
+  done
 
 theorem cp_thm:
   assumes lp: "iszlfm p"
-  and u: "d_\<beta> p 1"
-  and d: "d_\<delta> p d"
-  and dp: "d > 0"
+    and u: "d_\<beta> p 1"
+    and d: "d_\<delta> p d"
+    and dp: "d > 0"
   shows "(\<exists>(x::int). Ifm bbs (x #bs) p) = (\<exists>j\<in> {1.. d}. Ifm bbs (j #bs) (minusinf p) \<or> (\<exists>b \<in> set (\<beta> p). Ifm bbs ((Inum (i#bs) b + j) #bs) p))"
   (is "(\<exists>(x::int). ?P (x)) = (\<exists>j\<in> ?D. ?M j \<or> (\<exists>b\<in> ?B. ?P (?I b + j)))")
-proof-
+proof -
   from minusinf_inf[OF lp u]
-  have th: "\<exists>(z::int). \<forall>x<z. ?P (x) = ?M x" by blast
+  have th: "\<exists>(z::int). \<forall>x<z. ?P (x) = ?M x"
+    by blast
   let ?B' = "{?I b | b. b\<in> ?B}"
-  have BB': "(\<exists>j\<in>?D. \<exists>b\<in> ?B. ?P (?I b +j)) = (\<exists>j \<in> ?D. \<exists>b \<in> ?B'. ?P (b + j))" by auto
-  hence th2: "\<forall>x. \<not> (\<exists>j \<in> ?D. \<exists>b \<in> ?B'. ?P ((b + j))) \<longrightarrow> ?P (x) \<longrightarrow> ?P ((x - d))"
+  have BB': "(\<exists>j\<in>?D. \<exists>b\<in> ?B. ?P (?I b +j)) = (\<exists>j \<in> ?D. \<exists>b \<in> ?B'. ?P (b + j))"
+    by auto
+  then have th2: "\<forall>x. \<not> (\<exists>j \<in> ?D. \<exists>b \<in> ?B'. ?P ((b + j))) \<longrightarrow> ?P (x) \<longrightarrow> ?P ((x - d))"
     using \<beta>'[OF lp u d dp, where a="i" and bbs = "bbs"] by blast
   from minusinf_repeats[OF d lp]
-  have th3: "\<forall>x k. ?M x = ?M (x-k*d)" by simp
-  from cpmi_eq[OF dp th th2 th3] BB' show ?thesis by blast
+  have th3: "\<forall>x k. ?M x = ?M (x-k*d)"
+    by simp
+  from cpmi_eq[OF dp th th2 th3] BB' show ?thesis
+    by blast
 qed
 
-    (* Implement the right hand sides of Cooper's theorem and Ferrante and Rackoff. *)
+(* Implement the right hand sides of Cooper's theorem and Ferrante and Rackoff. *)
 lemma mirror_ex:
   assumes lp: "iszlfm p"
   shows "(\<exists>x. Ifm bbs (x#bs) (mirror p)) = (\<exists>x. Ifm bbs (x#bs) p)"
   (is "(\<exists>x. ?I x ?mp) = (\<exists>x. ?I x p)")
 proof(auto)
-  fix x assume "?I x ?mp" hence "?I (- x) p" using mirror[OF lp] by blast
-  thus "\<exists>x. ?I x p" by blast
+  fix x assume "?I x ?mp" then have "?I (- x) p" using mirror[OF lp] by blast
+  then show "\<exists>x. ?I x p" by blast
 next
-  fix x assume "?I x p" hence "?I (- x) ?mp"
+  fix x assume "?I x p" then have "?I (- x) ?mp"
     using mirror[OF lp, where x="- x", symmetric] by auto
-  thus "\<exists>x. ?I x ?mp" by blast
+  then show "\<exists>x. ?I x ?mp" by blast
 qed
 
 
@@ -2007,14 +2095,14 @@
   from \<alpha>_l[OF lq] have A_nb: "\<forall>b\<in> set ?A'. numbound0 b"
     by (simp add: simpnum_numbound0)
     {assume "length ?B' \<le> length ?A'"
-    hence q:"q=?q" and "B = ?B'" and d:"d = ?d"
+    then have q:"q=?q" and "B = ?B'" and d:"d = ?d"
       using qBd by (auto simp add: Let_def unit_def)
     with BB' B_nb have b: "?N ` (set B) = ?N ` set (\<beta> q)"
       and bn: "\<forall>b\<in> set B. numbound0 b" by simp_all
   with pq_ex dp uq dd lq q d have ?thes by simp}
   moreover
   {assume "\<not> (length ?B' \<le> length ?A')"
-    hence q:"q=mirror ?q" and "B = ?A'" and d:"d = ?d"
+    then have q:"q=mirror ?q" and "B = ?A'" and d:"d = ?d"
       using qBd by (auto simp add: Let_def unit_def)
     with AA' mirror_\<alpha>_\<beta>[OF lq] A_nb have b:"?N ` (set B) = ?N ` set (\<beta> q)"
       and bn: "\<forall>b\<in> set B. numbound0 b" by simp_all
@@ -2071,18 +2159,18 @@
   from zlin_qfree[OF lq] have qfq: "qfree ?q" .
   from simpfm_qf[OF minusinf_qfree[OF qfq]] have qfmq: "qfree ?smq".
   have jsnb: "\<forall>j \<in> set ?js. numbound0 (C j)" by simp
-  hence "\<forall>j\<in> set ?js. bound0 (subst0 (C j) ?smq)"
+  then have "\<forall>j\<in> set ?js. bound0 (subst0 (C j) ?smq)"
     by (auto simp only: subst0_bound0[OF qfmq])
-  hence th: "\<forall>j\<in> set ?js. bound0 (simpfm (subst0 (C j) ?smq))"
+  then have th: "\<forall>j\<in> set ?js. bound0 (simpfm (subst0 (C j) ?smq))"
     by (auto simp add: simpfm_bound0)
   from evaldjf_bound0[OF th] have mdb: "bound0 ?md" by simp
   from Bn jsnb have "\<forall>(b,j) \<in> set ?Bjs. numbound0 (Add b (C j))"
     by simp
-  hence "\<forall>(b,j) \<in> set ?Bjs. bound0 (subst0 (Add b (C j)) ?q)"
+  then have "\<forall>(b,j) \<in> set ?Bjs. bound0 (subst0 (Add b (C j)) ?q)"
     using subst0_bound0[OF qfq] by blast
-  hence "\<forall>(b,j) \<in> set ?Bjs. bound0 (simpfm (subst0 (Add b (C j)) ?q))"
+  then have "\<forall>(b,j) \<in> set ?Bjs. bound0 (simpfm (subst0 (Add b (C j)) ?q))"
     using simpfm_bound0  by blast
-  hence th': "\<forall>x \<in> set ?Bjs. bound0 ((\<lambda>(b,j). simpfm (subst0 (Add b (C j)) ?q)) x)"
+  then have th': "\<forall>x \<in> set ?Bjs. bound0 ((\<lambda>(b,j). simpfm (subst0 (Add b (C j)) ?q)) x)"
     by auto
   from evaldjf_bound0 [OF th'] have qdb: "bound0 ?qd" by simp
   from mdb qdb
@@ -2112,13 +2200,13 @@
   also have "\<dots> = (Ifm bbs bs (decr (disj ?md ?qd)))" by (simp only: decr [OF mdqdb])
   finally have mdqd2: "?lhs = (Ifm bbs bs (decr (disj ?md ?qd)))" .
   { assume mdT: "?md = T"
-    hence cT:"cooper p = T"
+    then have cT:"cooper p = T"
       by (simp only: cooper_def unit_def split_def Let_def if_True) simp
     from mdT have lhs:"?lhs" using mdqd by simp
     from mdT have "?rhs" by (simp add: cooper_def unit_def split_def)
     with lhs cT have ?thesis by simp }
   moreover
-  { assume mdT: "?md \<noteq> T" hence "cooper p = decr (disj ?md ?qd)"
+  { assume mdT: "?md \<noteq> T" then have "cooper p = decr (disj ?md ?qd)"
       by (simp only: cooper_def unit_def split_def Let_def if_False)
     with mdqd2 decr_qf[OF mdqdb] have ?thesis by simp }
   ultimately show ?thesis by blast
diff -r 6478b12b7297 -r b11b358fec57 src/Pure/General/path.scala
--- a/src/Pure/General/path.scala	Mon Mar 03 14:22:35 2014 +0100
+++ b/src/Pure/General/path.scala	Mon Mar 03 15:14:00 2014 +0100
@@ -97,9 +97,12 @@
     new Path(norm_elems(elems.reverse ::: roots))
   }
 
-  def is_ok(str: String): Boolean =
+  def is_wellformed(str: String): Boolean =
     try { explode(str); true } catch { case ERROR(_) => false }
 
+  def is_valid(str: String): Boolean =
+    try { explode(str).expand; true } catch { case ERROR(_) => false }
+
   def split(str: String): List[Path] =
     space_explode(':', str).filterNot(_.isEmpty).map(explode)
 
diff -r 6478b12b7297 -r b11b358fec57 src/Pure/General/position.scala
--- a/src/Pure/General/position.scala	Mon Mar 03 14:22:35 2014 +0100
+++ b/src/Pure/General/position.scala	Mon Mar 03 15:14:00 2014 +0100
@@ -50,8 +50,8 @@
 
   object Range
   {
-    def apply(range: Text.Range): T = Offset(range.start) ::: Offset(range.stop)
-    def unapply(pos: T): Option[Text.Range] =
+    def apply(range: Symbol.Range): T = Offset(range.start) ::: Offset(range.stop)
+    def unapply(pos: T): Option[Symbol.Range] =
       (pos, pos) match {
         case (Offset(start), End_Offset(stop)) if start <= stop => Some(Text.Range(start, stop))
         case (Offset(start), _) => Some(Text.Range(start, start + 1))
@@ -61,7 +61,7 @@
 
   object Id_Offset
   {
-    def unapply(pos: T): Option[(Long, Text.Offset)] =
+    def unapply(pos: T): Option[(Long, Symbol.Offset)] =
       (pos, pos) match {
         case (Id(id), Offset(offset)) => Some((id, offset))
         case _ => None
@@ -70,7 +70,7 @@
 
   object Def_Id_Offset
   {
-    def unapply(pos: T): Option[(Long, Text.Offset)] =
+    def unapply(pos: T): Option[(Long, Symbol.Offset)] =
       (pos, pos) match {
         case (Def_Id(id), Def_Offset(offset)) => Some((id, offset))
         case _ => None
@@ -79,7 +79,7 @@
 
   object Reported
   {
-    def unapply(pos: T): Option[(Long, String, Text.Range)] =
+    def unapply(pos: T): Option[(Long, String, Symbol.Range)] =
       (pos, pos) match {
         case (Id(id), Range(range)) =>
           Some((id, File.unapply(pos).getOrElse(""), range))
diff -r 6478b12b7297 -r b11b358fec57 src/Pure/General/symbol.scala
--- a/src/Pure/General/symbol.scala	Mon Mar 03 14:22:35 2014 +0100
+++ b/src/Pure/General/symbol.scala	Mon Mar 03 15:14:00 2014 +0100
@@ -16,6 +16,10 @@
 {
   type Symbol = String
 
+  // counting Isabelle symbols, starting from 1
+  type Offset = Text.Offset
+  type Range = Text.Range
+
 
   /* ASCII characters */
 
@@ -142,9 +146,9 @@
       buf.toArray
     }
 
-    def decode(sym1: Int): Int =
+    def decode(symbol_offset: Offset): Text.Offset =
     {
-      val sym = sym1 - 1
+      val sym = symbol_offset - 1
       val end = index.length
       @tailrec def bisect(a: Int, b: Int): Int =
       {
@@ -160,7 +164,7 @@
       if (i < 0) sym
       else index(i).chr + sym - index(i).sym
     }
-    def decode(range: Text.Range): Text.Range = range.map(decode(_))
+    def decode(symbol_range: Range): Text.Range = symbol_range.map(decode(_))
   }
 
 
diff -r 6478b12b7297 -r b11b358fec57 src/Pure/Isar/parse.scala
--- a/src/Pure/Isar/parse.scala	Mon Mar 03 14:22:35 2014 +0100
+++ b/src/Pure/Isar/parse.scala	Mon Mar 03 15:14:00 2014 +0100
@@ -62,9 +62,9 @@
     def ML_source: Parser[String] = atom("ML source", _.is_text)
     def document_source: Parser[String] = atom("document source", _.is_text)
     def path: Parser[String] =
-      atom("file name/path specification", tok => tok.is_name && Path.is_ok(tok.content))
+      atom("file name/path specification", tok => tok.is_name && Path.is_wellformed(tok.content))
     def theory_name: Parser[String] =
-      atom("theory name", tok => tok.is_name && Thy_Load.is_ok(tok.content))
+      atom("theory name", tok => tok.is_name && Thy_Load.is_wellformed(tok.content))
 
     private def tag_name: Parser[String] =
       atom("tag name", tok =>
diff -r 6478b12b7297 -r b11b358fec57 src/Pure/PIDE/command.scala
--- a/src/Pure/PIDE/command.scala	Mon Mar 03 14:22:35 2014 +0100
+++ b/src/Pure/PIDE/command.scala	Mon Mar 03 15:14:00 2014 +0100
@@ -152,11 +152,12 @@
               def bad(): Unit = System.err.println("Ignored report message: " + msg)
 
               msg match {
-                case XML.Elem(Markup(name, atts @ Position.Reported(id, file_name, raw_range)), args)
+                case XML.Elem(Markup(name,
+                  atts @ Position.Reported(id, file_name, symbol_range)), args)
                 if id == command.id || id == alt_id =>
                   command.chunks.get(file_name) match {
                     case Some(chunk) =>
-                      chunk.incorporate(raw_range) match {
+                      chunk.incorporate(symbol_range) match {
                         case Some(range) =>
                           val props = Position.purge(atts)
                           val info = Text.Info(range, XML.Elem(Markup(name, props), args))
@@ -216,16 +217,16 @@
     def file_name: String
     def length: Int
     def range: Text.Range
-    def decode(raw_range: Text.Range): Text.Range
+    def decode(symbol_range: Symbol.Range): Text.Range
 
-    def incorporate(raw_range: Text.Range): Option[Text.Range] =
+    def incorporate(symbol_range: Symbol.Range): Option[Text.Range] =
     {
-      def inc(r: Text.Range): Option[Text.Range] =
+      def inc(r: Symbol.Range): Option[Text.Range] =
         range.try_restrict(decode(r)) match {
           case Some(r1) if !r1.is_singularity => Some(r1)
           case _ => None
         }
-     inc(raw_range) orElse inc(raw_range - 1)
+     inc(symbol_range) orElse inc(symbol_range - 1)
     }
   }
 
@@ -234,7 +235,7 @@
     val length = text.length
     val range = Text.Range(0, length)
     private val symbol_index = Symbol.Index(text)
-    def decode(raw_range: Text.Range): Text.Range = symbol_index.decode(raw_range)
+    def decode(symbol_range: Symbol.Range): Text.Range = symbol_index.decode(symbol_range)
 
     override def toString: String = "Command.File(" + file_name + ")"
   }
@@ -374,8 +375,8 @@
   def source(range: Text.Range): String = source.substring(range.start, range.stop)
 
   private lazy val symbol_index = Symbol.Index(source)
-  def decode(raw_offset: Text.Offset): Text.Offset = symbol_index.decode(raw_offset)
-  def decode(raw_range: Text.Range): Text.Range = symbol_index.decode(raw_range)
+  def decode(symbol_offset: Symbol.Offset): Text.Offset = symbol_index.decode(symbol_offset)
+  def decode(symbol_range: Symbol.Range): Text.Range = symbol_index.decode(symbol_range)
 
 
   /* accumulated results */
diff -r 6478b12b7297 -r b11b358fec57 src/Pure/PIDE/editor.scala
--- a/src/Pure/PIDE/editor.scala	Mon Mar 03 14:22:35 2014 +0100
+++ b/src/Pure/PIDE/editor.scala	Mon Mar 03 15:14:00 2014 +0100
@@ -23,9 +23,7 @@
   def remove_overlay(command: Command, fn: String, args: List[String]): Unit
 
   abstract class Hyperlink { def follow(context: Context): Unit }
-  def hyperlink_url(name: String): Hyperlink
-  def hyperlink_file(file_name: String, line: Int = 0, column: Int = 0): Hyperlink
   def hyperlink_command(
-    snapshot: Document.Snapshot, command: Command, offset: Text.Offset = 0): Option[Hyperlink]
+    snapshot: Document.Snapshot, command: Command, offset: Symbol.Offset = 0): Option[Hyperlink]
 }
 
diff -r 6478b12b7297 -r b11b358fec57 src/Pure/PIDE/protocol.scala
--- a/src/Pure/PIDE/protocol.scala	Mon Mar 03 14:22:35 2014 +0100
+++ b/src/Pure/PIDE/protocol.scala	Mon Mar 03 15:14:00 2014 +0100
@@ -287,9 +287,9 @@
   {
     def elem_positions(props: Properties.T, set: Set[Text.Range]): Set[Text.Range] =
       props match {
-        case Position.Reported(id, file_name, raw_range)
+        case Position.Reported(id, file_name, symbol_range)
         if (id == command_id || id == alt_id) && file_name == chunk.file_name =>
-          chunk.incorporate(raw_range) match {
+          chunk.incorporate(symbol_range) match {
             case Some(range) => set + range
             case _ => set
           }
diff -r 6478b12b7297 -r b11b358fec57 src/Pure/System/isabelle_system.scala
--- a/src/Pure/System/isabelle_system.scala	Mon Mar 03 14:22:35 2014 +0100
+++ b/src/Pure/System/isabelle_system.scala	Mon Mar 03 15:14:00 2014 +0100
@@ -212,7 +212,8 @@
     if (path.is_absolute || path.is_current) check(path)
     else {
       check(Path.explode("~~/src/Pure") + path) orElse
-        (if (getenv("ML_SOURCES") == "") None else check(Path.explode("$ML_SOURCES") + path))
+        (if (getenv("ML_SOURCES") == "") None
+         else check(Path.explode("$ML_SOURCES") + path))
     }
   }
 
diff -r 6478b12b7297 -r b11b358fec57 src/Pure/Thy/thy_load.ML
--- a/src/Pure/Thy/thy_load.ML	Mon Mar 03 14:22:35 2014 +0100
+++ b/src/Pure/Thy/thy_load.ML	Mon Mar 03 15:14:00 2014 +0100
@@ -192,14 +192,25 @@
 
 (* document antiquotation *)
 
-fun file_antiq do_check ctxt (name, pos) =
+fun file_antiq strict ctxt (name, pos) =
   let
     val dir = master_directory (Proof_Context.theory_of ctxt);
-    val path = Path.append dir (Path.explode name);
+    val path = Path.append dir (Path.explode name)
+      handle ERROR msg => error (msg ^ Position.here pos);
+
+    val _ = Context_Position.report ctxt pos (Markup.path name);
     val _ =
-      if not do_check orelse File.exists path then ()
-      else error ("Bad file: " ^ Path.print (Path.expand path) ^ Position.here pos);
-    val _ = Context_Position.report ctxt pos (Markup.path name);
+      if can Path.expand path andalso File.exists path then ()
+      else
+        let
+          val path' = perhaps (try Path.expand) path;
+          val msg = "Bad file: " ^ Path.print path' ^ Position.here pos;
+        in
+          if strict then error msg
+          else
+            Context_Position.if_visible ctxt Output.report
+              (Markup.markup (Markup.bad |> Markup.properties (Position.properties_of pos)) msg)
+        end;
   in
     space_explode "/" name
     |> map Thy_Output.verb_text
diff -r 6478b12b7297 -r b11b358fec57 src/Pure/Thy/thy_load.scala
--- a/src/Pure/Thy/thy_load.scala	Mon Mar 03 14:22:35 2014 +0100
+++ b/src/Pure/Thy/thy_load.scala	Mon Mar 03 15:14:00 2014 +0100
@@ -18,7 +18,7 @@
 
   def thy_path(path: Path): Path = path.ext("thy")
 
-  def is_ok(str: String): Boolean =
+  def is_wellformed(str: String): Boolean =
     try { thy_path(Path.explode(str)); true }
     catch { case ERROR(_) => false }
 }
diff -r 6478b12b7297 -r b11b358fec57 src/Tools/jEdit/src/documentation_dockable.scala
--- a/src/Tools/jEdit/src/documentation_dockable.scala	Mon Mar 03 14:22:35 2014 +0100
+++ b/src/Tools/jEdit/src/documentation_dockable.scala	Mon Mar 03 15:14:00 2014 +0100
@@ -71,7 +71,7 @@
                         "Documentation error", GUI.scrollable_text(Exn.message(exn)))
                   })
               case Text_File(_, path) =>
-                PIDE.editor.goto(view, Isabelle_System.platform_path(path))
+                PIDE.editor.goto_file(view, Isabelle_System.platform_path(path))
               case _ =>
             }
           case _ =>
diff -r 6478b12b7297 -r b11b358fec57 src/Tools/jEdit/src/jedit_editor.scala
--- a/src/Tools/jEdit/src/jedit_editor.scala	Mon Mar 03 14:22:35 2014 +0100
+++ b/src/Tools/jEdit/src/jedit_editor.scala	Mon Mar 03 15:14:00 2014 +0100
@@ -109,9 +109,9 @@
     synchronized { overlays = overlays.remove(command, fn, args) }
 
 
-  /* hyperlinks */
+  /* navigation */
 
-  def goto(view: View, name: String, line: Int = 0, column: Int = 0)
+  def goto_file(view: View, name: String, line: Int = 0, column: Int = 0)
   {
     Swing_Thread.require()
 
@@ -142,7 +142,68 @@
     }
   }
 
-  override def hyperlink_url(name: String): Hyperlink =
+
+  /* hyperlinks */
+
+  override def hyperlink_command(
+    snapshot: Document.Snapshot, command: Command, offset: Symbol.Offset = 0): Option[Hyperlink] =
+  {
+    if (snapshot.is_outdated) None
+    else {
+      snapshot.state.find_command(snapshot.version, command.id) match {
+        case None => None
+        case Some((node, _)) =>
+          val file_name = command.node_name.node
+          val sources =
+            node.commands.iterator.takeWhile(_ != command).map(_.source) ++
+              (if (offset == 0) Iterator.empty
+               else Iterator.single(command.source(Text.Range(0, command.decode(offset)))))
+          val (line, column) = ((1, 1) /: sources)(Symbol.advance_line_column)
+          Some(new Hyperlink { def follow(view: View) { goto_file(view, file_name, line, column) } })
+      }
+    }
+  }
+
+  def hyperlink_command_id(
+    snapshot: Document.Snapshot,
+    id: Document_ID.Generic,
+    offset: Symbol.Offset): Option[Hyperlink] =
+  {
+    snapshot.state.find_command(snapshot.version, id) match {
+      case Some((node, command)) => hyperlink_command(snapshot, command, offset)
+      case None => None
+    }
+  }
+
+  def hyperlink_file(name: String, line: Int = 0, column: Int = 0): Hyperlink =
+    new Hyperlink { def follow(view: View) = goto_file(view, name, line, column) }
+
+  def hyperlink_source_file(source_name: String, line: Int, offset: Symbol.Offset)
+    : Option[Hyperlink] =
+  {
+    if (Path.is_valid(source_name)) {
+      Isabelle_System.source_file(Path.explode(source_name)) match {
+        case Some(path) =>
+          val name = Isabelle_System.platform_path(path)
+          JEdit_Lib.jedit_buffer(name) match {
+            case Some(buffer) if offset > 0 =>
+              val (line, column) =
+                JEdit_Lib.buffer_lock(buffer) {
+                  ((1, 1) /:
+                    (Symbol.iterator(JEdit_Lib.buffer_text(buffer)).
+                      zipWithIndex.takeWhile(p => p._2 < offset - 1).map(_._1)))(
+                        Symbol.advance_line_column)
+                }
+              Some(hyperlink_file(name, line, column))
+            case _ => Some(hyperlink_file(name, line))
+          }
+        case None => None
+      }
+    }
+    else None
+  }
+
+  def hyperlink_url(name: String): Hyperlink =
     new Hyperlink {
       def follow(view: View) =
         default_thread_pool.submit(() =>
@@ -152,26 +213,4 @@
               GUI.error_dialog(view, "System error", GUI.scrollable_text(Exn.message(exn)))
           })
     }
-
-  override def hyperlink_file(name: String, line: Int = 0, column: Int = 0): Hyperlink =
-    new Hyperlink { def follow(view: View) = goto(view, name, line, column) }
-
-  override def hyperlink_command(snapshot: Document.Snapshot, command: Command, raw_offset: Int = 0)
-    : Option[Hyperlink] =
-  {
-    if (snapshot.is_outdated) None
-    else {
-      snapshot.state.find_command(snapshot.version, command.id) match {
-        case None => None
-        case Some((node, _)) =>
-          val file_name = command.node_name.node
-          val sources =
-            node.commands.iterator.takeWhile(_ != command).map(_.source) ++
-              (if (raw_offset == 0) Iterator.empty
-               else Iterator.single(command.source(Text.Range(0, command.decode(raw_offset)))))
-          val (line, column) = ((1, 1) /: sources)(Symbol.advance_line_column)
-          Some(new Hyperlink { def follow(view: View) { goto(view, file_name, line, column) } })
-      }
-    }
-  }
 }
diff -r 6478b12b7297 -r b11b358fec57 src/Tools/jEdit/src/rendering.scala
--- a/src/Tools/jEdit/src/rendering.scala	Mon Mar 03 14:22:35 2014 +0100
+++ b/src/Tools/jEdit/src/rendering.scala	Mon Mar 03 15:14:00 2014 +0100
@@ -327,27 +327,13 @@
 
   /* hyperlinks */
 
-  private def hyperlink_file(line: Int, name: String): Option[PIDE.editor.Hyperlink] =
-    if (Path.is_ok(name))
-      Isabelle_System.source_file(Path.explode(name)).map(path =>
-        PIDE.editor.hyperlink_file(Isabelle_System.platform_path(path), line))
-    else None
-
-  private def hyperlink_command(id: Document_ID.Generic, offset: Text.Offset)
-      : Option[PIDE.editor.Hyperlink] =
-    snapshot.state.find_command(snapshot.version, id) match {
-      case Some((node, command)) =>
-        PIDE.editor.hyperlink_command(snapshot, command, offset)
-      case None => None
-    }
-
   def hyperlink(range: Text.Range): Option[Text.Info[PIDE.editor.Hyperlink]] =
   {
     snapshot.cumulate[Vector[Text.Info[PIDE.editor.Hyperlink]]](
       range, Vector.empty, Rendering.hyperlink_elements, _ =>
         {
           case (links, Text.Info(info_range, XML.Elem(Markup.Path(name), _)))
-          if Path.is_ok(name) =>
+          if Path.is_valid(name) =>
             val jedit_file = PIDE.thy_load.append(snapshot.node_name.master_dir, Path.explode(name))
             val link = PIDE.editor.hyperlink_file(jedit_file)
             Some(links :+ Text.Info(snapshot.convert(info_range), link))
@@ -361,11 +347,13 @@
             { case (Markup.KIND, Markup.ML_OPEN) => true
               case (Markup.KIND, Markup.ML_STRUCTURE) => true
               case _ => false }) =>
-
             val opt_link =
               props match {
-                case Position.Def_Line_File(line, name) => hyperlink_file(line, name)
-                case Position.Def_Id_Offset(id, offset) => hyperlink_command(id, offset)
+                case Position.Def_Line_File(line, name) =>
+                  val offset = Position.Def_Offset.unapply(props) getOrElse 0
+                  PIDE.editor.hyperlink_source_file(name, line, offset)
+                case Position.Def_Id_Offset(id, offset) =>
+                  PIDE.editor.hyperlink_command_id(snapshot, id, offset)
                 case _ => None
               }
             opt_link.map(link => (links :+ Text.Info(snapshot.convert(info_range), link)))
@@ -373,11 +361,14 @@
           case (links, Text.Info(info_range, XML.Elem(Markup(Markup.POSITION, props), _))) =>
             val opt_link =
               props match {
-                case Position.Line_File(line, name) => hyperlink_file(line, name)
-                case Position.Id_Offset(id, offset) => hyperlink_command(id, offset)
+                case Position.Line_File(line, name) =>
+                  val offset = Position.Offset.unapply(props) getOrElse 0
+                  PIDE.editor.hyperlink_source_file(name, line, offset)
+                case Position.Id_Offset(id, offset) =>
+                  PIDE.editor.hyperlink_command_id(snapshot, id, offset)
                 case _ => None
               }
-            opt_link.map(link => links :+ (Text.Info(snapshot.convert(info_range), link)))
+            opt_link.map(link => (links :+ Text.Info(snapshot.convert(info_range), link)))
 
           case _ => None
         }) match { case Text.Info(_, _ :+ info) :: _ => Some(info) case _ => None }
@@ -476,7 +467,7 @@
               else ""
             Some(add(prev, r, (true, XML.Text(txt1 + txt2))))
           case (prev, Text.Info(r, XML.Elem(Markup.Path(name), _)))
-          if Path.is_ok(name) =>
+          if Path.is_valid(name) =>
             val jedit_file = PIDE.thy_load.append(snapshot.node_name.master_dir, Path.explode(name))
             Some(add(prev, r, (true, XML.Text("file " + quote(jedit_file)))))
           case (prev, Text.Info(r, XML.Elem(Markup.Url(name), _))) =>
diff -r 6478b12b7297 -r b11b358fec57 src/Tools/jEdit/src/theories_dockable.scala
--- a/src/Tools/jEdit/src/theories_dockable.scala	Mon Mar 03 14:22:35 2014 +0100
+++ b/src/Tools/jEdit/src/theories_dockable.scala	Mon Mar 03 15:14:00 2014 +0100
@@ -40,7 +40,7 @@
               } model.node_required = !model.node_required
             }
           }
-          else if (clicks == 2) PIDE.editor.goto(view, listData(index).node)
+          else if (clicks == 2) PIDE.editor.goto_file(view, listData(index).node)
         }
       case MouseMoved(_, point, _) =>
         val index = peer.locationToIndex(point)
diff -r 6478b12b7297 -r b11b358fec57 src/Tools/jEdit/src/timing_dockable.scala
--- a/src/Tools/jEdit/src/timing_dockable.scala	Mon Mar 03 14:22:35 2014 +0100
+++ b/src/Tools/jEdit/src/timing_dockable.scala	Mon Mar 03 15:14:00 2014 +0100
@@ -88,7 +88,7 @@
     extends Entry
   {
     def print: String = Time.print_seconds(timing) + "s theory " + quote(name.theory)
-    def follow(snapshot: Document.Snapshot) { PIDE.editor.goto(view, name.node) }
+    def follow(snapshot: Document.Snapshot) { PIDE.editor.goto_file(view, name.node) }
   }
 
   private case class Command_Entry(command: Command, timing: Double) extends Entry