# HG changeset patch
# User blanchet
# Date 1280911949 -7200
# Node ID 1a1973c005317c2920871a00a06f73d4961b4e05
# Parent  05691ad7407976d0dca6ee46304e94f1990b49c1# Parent  deaef70a8c058b75fa94f8912fcc65bced474c59
merged

diff -r deaef70a8c05 -r 1a1973c00531 NEWS
--- a/NEWS	Wed Aug 04 10:51:04 2010 +0200
+++ b/NEWS	Wed Aug 04 10:52:29 2010 +0200
@@ -14,6 +14,10 @@
 consistent view on symbols, while raw explode (or String.explode)
 merely give a byte-oriented representation.
 
+* Theory loading: only the master source file is looked-up in the
+implicit load path, all other files are addressed relatively to its
+directory.  Minor INCOMPATIBILITY, subtle change in semantics.
+
 * Special treatment of ML file names has been discontinued.
 Historically, optional extensions .ML or .sml were added on demand --
 at the cost of clarity of file dependencies.  Recall that Isabelle/ML
diff -r deaef70a8c05 -r 1a1973c00531 src/HOL/Algebra/UnivPoly.thy
--- a/src/HOL/Algebra/UnivPoly.thy	Wed Aug 04 10:51:04 2010 +0200
+++ b/src/HOL/Algebra/UnivPoly.thy	Wed Aug 04 10:52:29 2010 +0200
@@ -1557,128 +1557,93 @@
   assumes g_in_P [simp]: "g \<in> carrier P" and f_in_P [simp]: "f \<in> carrier P"
   and g_not_zero: "g \<noteq> \<zero>\<^bsub>P\<^esub>"
   shows "\<exists> q r (k::nat). (q \<in> carrier P) \<and> (r \<in> carrier P) \<and> (lcoeff g)(^)\<^bsub>R\<^esub>k \<odot>\<^bsub>P\<^esub> f = g \<otimes>\<^bsub>P\<^esub> q \<oplus>\<^bsub>P\<^esub> r \<and> (r = \<zero>\<^bsub>P\<^esub> | deg R r < deg R g)"
-proof -
+  using f_in_P
+proof (induct "deg R f" arbitrary: "f" rule: nat_less_induct)
+  case (1 f)
+  note f_in_P [simp] = "1.prems"
   let ?pred = "(\<lambda> q r (k::nat).
-    (q \<in> carrier P) \<and> (r \<in> carrier P) \<and> (lcoeff g)(^)\<^bsub>R\<^esub>k \<odot>\<^bsub>P\<^esub> f = g \<otimes>\<^bsub>P\<^esub> q \<oplus>\<^bsub>P\<^esub> r \<and> (r = \<zero>\<^bsub>P\<^esub> | deg R r < deg R g))"
-    and ?lg = "lcoeff g"
-  show ?thesis
-    (*JE: we distinguish some particular cases where the solution is almost direct.*)
+    (q \<in> carrier P) \<and> (r \<in> carrier P) 
+    \<and> (lcoeff g)(^)\<^bsub>R\<^esub>k \<odot>\<^bsub>P\<^esub> f = g \<otimes>\<^bsub>P\<^esub> q \<oplus>\<^bsub>P\<^esub> r \<and> (r = \<zero>\<^bsub>P\<^esub> | deg R r < deg R g))"
+  let ?lg = "lcoeff g" and ?lf = "lcoeff f"
+  show ?case
   proof (cases "deg R f < deg R g")
-    case True     
-      (*JE: if the degree of f is smaller than the one of g the solution is straightforward.*)
-      (* CB: avoid exI3 *)
-      have "?pred \<zero>\<^bsub>P\<^esub> f 0" using True by force
-      then show ?thesis by fast
+    case True
+    have "?pred \<zero>\<^bsub>P\<^esub> f 0" using True by force
+    then show ?thesis by blast
   next
     case False then have deg_g_le_deg_f: "deg R g \<le> deg R f" by simp
     {
-      (*JE: we now apply the induction hypothesis with some additional facts required*)
-      from f_in_P deg_g_le_deg_f show ?thesis
-      proof (induct "deg R f" arbitrary: "f" rule: less_induct)
-        case less
-        note f_in_P [simp] = `f \<in> carrier P`
-          and deg_g_le_deg_f = `deg R g \<le> deg R f`
-        let ?k = "1::nat" and ?r = "(g \<otimes>\<^bsub>P\<^esub> (monom P (lcoeff f) (deg R f - deg R g))) \<oplus>\<^bsub>P\<^esub> \<ominus>\<^bsub>P\<^esub> (lcoeff g \<odot>\<^bsub>P\<^esub> f)"
-          and ?q = "monom P (lcoeff f) (deg R f - deg R g)"
-        show "\<exists> q r (k::nat). q \<in> carrier P \<and> r \<in> carrier P \<and> lcoeff g (^) k \<odot>\<^bsub>P\<^esub> f = g \<otimes>\<^bsub>P\<^esub> q \<oplus>\<^bsub>P\<^esub> r & (r = \<zero>\<^bsub>P\<^esub> | deg R r < deg R g)"
-        proof -
-          (*JE: we first extablish the existence of a triple satisfying the previous equation. 
-            Then we will have to prove the second part of the predicate.*)
-          have exist: "lcoeff g (^) ?k \<odot>\<^bsub>P\<^esub> f = g \<otimes>\<^bsub>P\<^esub> ?q \<oplus>\<^bsub>P\<^esub> \<ominus>\<^bsub>P\<^esub> ?r"
-            using minus_add
-            using sym [OF a_assoc [of "g \<otimes>\<^bsub>P\<^esub> ?q" "\<ominus>\<^bsub>P\<^esub> (g \<otimes>\<^bsub>P\<^esub> ?q)" "lcoeff g \<odot>\<^bsub>P\<^esub> f"]]
-            using r_neg by auto
+      let ?k = "1::nat"
+      let ?f1 = "(g \<otimes>\<^bsub>P\<^esub> (monom P (?lf) (deg R f - deg R g))) \<oplus>\<^bsub>P\<^esub> \<ominus>\<^bsub>P\<^esub> (?lg \<odot>\<^bsub>P\<^esub> f)"
+      let ?q = "monom P (?lf) (deg R f - deg R g)"
+      have f1_in_carrier: "?f1 \<in> carrier P" and q_in_carrier: "?q \<in> carrier P" by simp_all
+      show ?thesis
+      proof (cases "deg R f = 0")
+        case True
+        {
+          have deg_g: "deg R g = 0" using True using deg_g_le_deg_f by simp
+          have "?pred f \<zero>\<^bsub>P\<^esub> 1"
+            using deg_zero_impl_monom [OF g_in_P deg_g]
+            using sym [OF monom_mult_is_smult [OF coeff_closed [OF g_in_P, of 0] f_in_P]]
+            using deg_g by simp
+          then show ?thesis by blast
+        }
+      next
+        case False note deg_f_nzero = False
+        {
+          have exist: "lcoeff g (^) ?k \<odot>\<^bsub>P\<^esub> f = g \<otimes>\<^bsub>P\<^esub> ?q \<oplus>\<^bsub>P\<^esub> \<ominus>\<^bsub>P\<^esub> ?f1"
+            by (simp add: minus_add r_neg sym [
+              OF a_assoc [of "g \<otimes>\<^bsub>P\<^esub> ?q" "\<ominus>\<^bsub>P\<^esub> (g \<otimes>\<^bsub>P\<^esub> ?q)" "lcoeff g \<odot>\<^bsub>P\<^esub> f"]])
+          have deg_remainder_l_f: "deg R (\<ominus>\<^bsub>P\<^esub> ?f1) < deg R f"
+          proof (unfold deg_uminus [OF f1_in_carrier])
+            show "deg R ?f1 < deg R f"
+            proof (rule deg_lcoeff_cancel)
+              show "deg R (\<ominus>\<^bsub>P\<^esub> (?lg \<odot>\<^bsub>P\<^esub> f)) \<le> deg R f"
+                using deg_smult_ring [of ?lg f]
+                using lcoeff_nonzero2 [OF g_in_P g_not_zero] by simp
+              show "deg R (g \<otimes>\<^bsub>P\<^esub> ?q) \<le> deg R f"
+                by (simp add: monom_deg_mult [OF f_in_P g_in_P deg_g_le_deg_f, of ?lf])
+              show "coeff P (g \<otimes>\<^bsub>P\<^esub> ?q) (deg R f) = \<ominus> coeff P (\<ominus>\<^bsub>P\<^esub> (?lg \<odot>\<^bsub>P\<^esub> f)) (deg R f)"
+                unfolding coeff_mult [OF g_in_P monom_closed 
+                  [OF lcoeff_closed [OF f_in_P], 
+                    of "deg R f - deg R g"], of "deg R f"]
+                unfolding coeff_monom [OF lcoeff_closed 
+                  [OF f_in_P], of "(deg R f - deg R g)"]
+                using R.finsum_cong' [of "{..deg R f}" "{..deg R f}" 
+                  "(\<lambda>i. coeff P g i \<otimes> (if deg R f - deg R g = deg R f - i then ?lf else \<zero>))" 
+                  "(\<lambda>i. if deg R g = i then coeff P g i \<otimes> ?lf else \<zero>)"]
+                using R.finsum_singleton [of "deg R g" "{.. deg R f}" "(\<lambda>i. coeff P g i \<otimes> ?lf)"]
+                unfolding Pi_def using deg_g_le_deg_f by force
+            qed (simp_all add: deg_f_nzero)
+          qed
+          then obtain q' r' k'
+            where rem_desc: "?lg (^) (k'::nat) \<odot>\<^bsub>P\<^esub> (\<ominus>\<^bsub>P\<^esub> ?f1) = g \<otimes>\<^bsub>P\<^esub> q' \<oplus>\<^bsub>P\<^esub> r'"
+            and rem_deg: "(r' = \<zero>\<^bsub>P\<^esub> \<or> deg R r' < deg R g)"
+            and q'_in_carrier: "q' \<in> carrier P" and r'_in_carrier: "r' \<in> carrier P"
+            using "1.hyps" using f1_in_carrier by blast
           show ?thesis
-          proof (cases "deg R (\<ominus>\<^bsub>P\<^esub> ?r) < deg R g")
-            (*JE: if the degree of the remainder satisfies the statement property we are done*)
-            case True
-            {
-              show ?thesis
-              proof (rule exI3 [of _ ?q "\<ominus>\<^bsub>P\<^esub> ?r" ?k], intro conjI)
-                show "lcoeff g (^) ?k \<odot>\<^bsub>P\<^esub> f = g \<otimes>\<^bsub>P\<^esub> ?q \<oplus>\<^bsub>P\<^esub> \<ominus>\<^bsub>P\<^esub> ?r" using exist by simp
-                show "\<ominus>\<^bsub>P\<^esub> ?r = \<zero>\<^bsub>P\<^esub> \<or> deg R (\<ominus>\<^bsub>P\<^esub> ?r) < deg R g" using True by simp
-              qed (simp_all)
-            }
-          next
-            case False note n_deg_r_l_deg_g = False
-            {
-              (*JE: otherwise, we verify the conditions of the induction hypothesis.*)
-              show ?thesis
-              proof (cases "deg R f = 0")
-                (*JE: the solutions are different if the degree of f is zero or not*)
-                case True
-                {
-                  have deg_g: "deg R g = 0" using True using deg_g_le_deg_f by simp
-                  have "lcoeff g (^) (1::nat) \<odot>\<^bsub>P\<^esub> f = g \<otimes>\<^bsub>P\<^esub> f \<oplus>\<^bsub>P\<^esub> \<zero>\<^bsub>P\<^esub>"
-                    unfolding deg_g apply simp
-                    unfolding sym [OF monom_mult_is_smult [OF coeff_closed [OF g_in_P, of 0] f_in_P]]
-                    using deg_zero_impl_monom [OF g_in_P deg_g] by simp
-                  then show ?thesis using f_in_P by blast
-                }
-              next
-                case False note deg_f_nzero = False
-                {
-                  (*JE: now it only remains the case where the induction hypothesis can be used.*)
-                  (*JE: we first prove that the degree of the remainder is smaller than the one of f*)
-                  have deg_remainder_l_f: "deg R (\<ominus>\<^bsub>P\<^esub> ?r) < deg R f"
-                  proof -
-                    have "deg R (\<ominus>\<^bsub>P\<^esub> ?r) = deg R ?r" using deg_uminus [of ?r] by simp
-                    also have "\<dots> < deg R f"
-                    proof (rule deg_lcoeff_cancel)
-                      show "deg R (\<ominus>\<^bsub>P\<^esub> (lcoeff g \<odot>\<^bsub>P\<^esub> f)) \<le> deg R f"
-                        using deg_smult_ring [of "lcoeff g" f]
-                        using lcoeff_nonzero2 [OF g_in_P g_not_zero] by simp
-                      show "deg R (g \<otimes>\<^bsub>P\<^esub> ?q) \<le> deg R f"
-                        using monom_deg_mult [OF _ g_in_P, of f "lcoeff f"] and deg_g_le_deg_f
-                        by simp
-                      show "coeff P (g \<otimes>\<^bsub>P\<^esub> ?q) (deg R f) = \<ominus> coeff P (\<ominus>\<^bsub>P\<^esub> (lcoeff g \<odot>\<^bsub>P\<^esub> f)) (deg R f)"
-                        unfolding coeff_mult [OF g_in_P monom_closed [OF lcoeff_closed [OF f_in_P], of "deg R f - deg R g"], of "deg R f"]
-                        unfolding coeff_monom [OF lcoeff_closed [OF f_in_P], of "(deg R f - deg R g)"]
-                        using R.finsum_cong' [of "{..deg R f}" "{..deg R f}" 
-                          "(\<lambda>i. coeff P g i \<otimes> (if deg R f - deg R g = deg R f - i then lcoeff f else \<zero>))" 
-                          "(\<lambda>i. if deg R g = i then coeff P g i \<otimes> lcoeff f else \<zero>)"]
-                        using R.finsum_singleton [of "deg R g" "{.. deg R f}" "(\<lambda>i. coeff P g i \<otimes> lcoeff f)"]
-                        unfolding Pi_def using deg_g_le_deg_f by force
-                    qed (simp_all add: deg_f_nzero)
-                    finally show "deg R (\<ominus>\<^bsub>P\<^esub> ?r) < deg R f" .
-                  qed
-                  moreover have "\<ominus>\<^bsub>P\<^esub> ?r \<in> carrier P" by simp
-                  moreover obtain m where deg_rem_eq_m: "deg R (\<ominus>\<^bsub>P\<^esub> ?r) = m" by auto
-                  moreover have "deg R g \<le> deg R (\<ominus>\<^bsub>P\<^esub> ?r)" using n_deg_r_l_deg_g by simp
-                    (*JE: now, by applying the induction hypothesis, we obtain new quotient, remainder and exponent.*)
-                  ultimately obtain q' r' k'
-                    where rem_desc: "lcoeff g (^) (k'::nat) \<odot>\<^bsub>P\<^esub> (\<ominus>\<^bsub>P\<^esub> ?r) = g \<otimes>\<^bsub>P\<^esub> q' \<oplus>\<^bsub>P\<^esub> r'"and rem_deg: "(r' = \<zero>\<^bsub>P\<^esub> \<or> deg R r' < deg R g)"
-                    and q'_in_carrier: "q' \<in> carrier P" and r'_in_carrier: "r' \<in> carrier P"
-                    using less by blast
-                      (*JE: we now prove that the new quotient, remainder and exponent can be used to get 
-                      the quotient, remainder and exponent of the long division theorem*)
-                  show ?thesis
-                  proof (rule exI3 [of _ "((lcoeff g (^) k') \<odot>\<^bsub>P\<^esub> ?q \<oplus>\<^bsub>P\<^esub> q')" r' "Suc k'"], intro conjI)
-                    show "(lcoeff g (^) (Suc k')) \<odot>\<^bsub>P\<^esub> f = g \<otimes>\<^bsub>P\<^esub> ((lcoeff g (^) k') \<odot>\<^bsub>P\<^esub> ?q \<oplus>\<^bsub>P\<^esub> q') \<oplus>\<^bsub>P\<^esub> r'"
-                    proof -
-                      have "(lcoeff g (^) (Suc k')) \<odot>\<^bsub>P\<^esub> f = (lcoeff g (^) k') \<odot>\<^bsub>P\<^esub> (g \<otimes>\<^bsub>P\<^esub> ?q \<oplus>\<^bsub>P\<^esub> \<ominus>\<^bsub>P\<^esub> ?r)" 
-                        using smult_assoc1 exist by simp
-                      also have "\<dots> = (lcoeff g (^) k') \<odot>\<^bsub>P\<^esub> (g \<otimes>\<^bsub>P\<^esub> ?q) \<oplus>\<^bsub>P\<^esub> ((lcoeff g (^) k') \<odot>\<^bsub>P\<^esub> ( \<ominus>\<^bsub>P\<^esub> ?r))"
-                        using UP_smult_r_distr by simp
-                      also have "\<dots> = (lcoeff g (^) k') \<odot>\<^bsub>P\<^esub> (g \<otimes>\<^bsub>P\<^esub> ?q) \<oplus>\<^bsub>P\<^esub> (g \<otimes>\<^bsub>P\<^esub> q' \<oplus>\<^bsub>P\<^esub> r')"
-                        using rem_desc by simp
-                      also have "\<dots> = (lcoeff g (^) k') \<odot>\<^bsub>P\<^esub> (g \<otimes>\<^bsub>P\<^esub> ?q) \<oplus>\<^bsub>P\<^esub> g \<otimes>\<^bsub>P\<^esub> q' \<oplus>\<^bsub>P\<^esub> r'"
-                        using sym [OF a_assoc [of "lcoeff g (^) k' \<odot>\<^bsub>P\<^esub> (g \<otimes>\<^bsub>P\<^esub> ?q)" "g \<otimes>\<^bsub>P\<^esub> q'" "r'"]]
-                        using q'_in_carrier r'_in_carrier by simp
-                      also have "\<dots> = (lcoeff g (^) k') \<odot>\<^bsub>P\<^esub> (?q \<otimes>\<^bsub>P\<^esub> g) \<oplus>\<^bsub>P\<^esub> q' \<otimes>\<^bsub>P\<^esub> g \<oplus>\<^bsub>P\<^esub> r'"
-                        using q'_in_carrier by (auto simp add: m_comm)
-                      also have "\<dots> = (((lcoeff g (^) k') \<odot>\<^bsub>P\<^esub> ?q) \<otimes>\<^bsub>P\<^esub> g) \<oplus>\<^bsub>P\<^esub> q' \<otimes>\<^bsub>P\<^esub> g \<oplus>\<^bsub>P\<^esub> r'" 
-                        using smult_assoc2 q'_in_carrier by auto
-                      also have "\<dots> = ((lcoeff g (^) k') \<odot>\<^bsub>P\<^esub> ?q \<oplus>\<^bsub>P\<^esub> q') \<otimes>\<^bsub>P\<^esub> g \<oplus>\<^bsub>P\<^esub> r'"
-                        using sym [OF l_distr] and q'_in_carrier by auto
-                      finally show ?thesis using m_comm q'_in_carrier by auto
-                    qed
-                  qed (simp_all add: rem_deg q'_in_carrier r'_in_carrier)
-                }
-              qed
-            }
-          qed
-        qed
+          proof (rule exI3 [of _ "((?lg (^) k') \<odot>\<^bsub>P\<^esub> ?q \<oplus>\<^bsub>P\<^esub> q')" r' "Suc k'"], intro conjI)
+            show "(?lg (^) (Suc k')) \<odot>\<^bsub>P\<^esub> f = g \<otimes>\<^bsub>P\<^esub> ((?lg (^) k') \<odot>\<^bsub>P\<^esub> ?q \<oplus>\<^bsub>P\<^esub> q') \<oplus>\<^bsub>P\<^esub> r'"
+            proof -
+              have "(?lg (^) (Suc k')) \<odot>\<^bsub>P\<^esub> f = (?lg (^) k') \<odot>\<^bsub>P\<^esub> (g \<otimes>\<^bsub>P\<^esub> ?q \<oplus>\<^bsub>P\<^esub> \<ominus>\<^bsub>P\<^esub> ?f1)"
+                using smult_assoc1 [OF _ _ f_in_P] using exist by simp
+              also have "\<dots> = (?lg (^) k') \<odot>\<^bsub>P\<^esub> (g \<otimes>\<^bsub>P\<^esub> ?q) \<oplus>\<^bsub>P\<^esub> ((?lg (^) k') \<odot>\<^bsub>P\<^esub> ( \<ominus>\<^bsub>P\<^esub> ?f1))"
+                using UP_smult_r_distr by simp
+              also have "\<dots> = (?lg (^) k') \<odot>\<^bsub>P\<^esub> (g \<otimes>\<^bsub>P\<^esub> ?q) \<oplus>\<^bsub>P\<^esub> (g \<otimes>\<^bsub>P\<^esub> q' \<oplus>\<^bsub>P\<^esub> r')"
+                unfolding rem_desc ..
+              also have "\<dots> = (?lg (^) k') \<odot>\<^bsub>P\<^esub> (g \<otimes>\<^bsub>P\<^esub> ?q) \<oplus>\<^bsub>P\<^esub> g \<otimes>\<^bsub>P\<^esub> q' \<oplus>\<^bsub>P\<^esub> r'"
+                using sym [OF a_assoc [of "?lg (^) k' \<odot>\<^bsub>P\<^esub> (g \<otimes>\<^bsub>P\<^esub> ?q)" "g \<otimes>\<^bsub>P\<^esub> q'" "r'"]]
+                using r'_in_carrier q'_in_carrier by simp
+              also have "\<dots> = (?lg (^) k') \<odot>\<^bsub>P\<^esub> (?q \<otimes>\<^bsub>P\<^esub> g) \<oplus>\<^bsub>P\<^esub> q' \<otimes>\<^bsub>P\<^esub> g \<oplus>\<^bsub>P\<^esub> r'"
+                using q'_in_carrier by (auto simp add: m_comm)
+              also have "\<dots> = (((?lg (^) k') \<odot>\<^bsub>P\<^esub> ?q) \<otimes>\<^bsub>P\<^esub> g) \<oplus>\<^bsub>P\<^esub> q' \<otimes>\<^bsub>P\<^esub> g \<oplus>\<^bsub>P\<^esub> r'" 
+                using smult_assoc2 q'_in_carrier "1.prems" by auto
+              also have "\<dots> = ((?lg (^) k') \<odot>\<^bsub>P\<^esub> ?q \<oplus>\<^bsub>P\<^esub> q') \<otimes>\<^bsub>P\<^esub> g \<oplus>\<^bsub>P\<^esub> r'"
+                using sym [OF l_distr] and q'_in_carrier by auto
+              finally show ?thesis using m_comm q'_in_carrier by auto
+            qed
+          qed (simp_all add: rem_deg q'_in_carrier r'_in_carrier)
+        }
       qed
     }
   qed
diff -r deaef70a8c05 -r 1a1973c00531 src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy
--- a/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy	Wed Aug 04 10:51:04 2010 +0200
+++ b/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy	Wed Aug 04 10:52:29 2010 +0200
@@ -5,8 +5,8 @@
 header{* A formalization of Ferrante and Rackoff's procedure with polynomial parameters, see Paper in CALCULEMUS 2008 *}
 
 theory Parametric_Ferrante_Rackoff
-imports Reflected_Multivariate_Polynomial 
-  "~~/src/HOL/Decision_Procs/Dense_Linear_Order"
+imports Reflected_Multivariate_Polynomial
+  Dense_Linear_Order
   Efficient_Nat
 begin
 
diff -r deaef70a8c05 -r 1a1973c00531 src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Wed Aug 04 10:51:04 2010 +0200
+++ b/src/HOL/IsaMakefile	Wed Aug 04 10:52:29 2010 +0200
@@ -395,16 +395,16 @@
 
 HOL-Library: HOL $(OUT)/HOL-Library
 
-$(OUT)/HOL-Library: $(OUT)/HOL Library/HOL_Library_ROOT.ML		\
+$(OUT)/HOL-Library: $(OUT)/HOL Library/ROOT.ML				\
   $(SRC)/HOL/Tools/float_arith.ML $(SRC)/Tools/float.ML			\
   Library/Abstract_Rat.thy $(SRC)/Tools/Adhoc_Overloading.thy		\
-  Library/AssocList.thy	Library/BigO.thy Library/Binomial.thy		\
+  Library/AssocList.thy Library/BigO.thy Library/Binomial.thy		\
   Library/Bit.thy Library/Boolean_Algebra.thy Library/Cardinality.thy	\
   Library/Char_nat.thy Library/Code_Char.thy Library/Code_Char_chr.thy	\
-  Library/Code_Integer.thy Library/Code_Natural.thy 			\
+  Library/Code_Integer.thy Library/Code_Natural.thy			\
   Library/Code_Prolog.thy Tools/Predicate_Compile/code_prolog.ML	\
   Library/ContNotDenum.thy Library/Continuity.thy Library/Convex.thy	\
-  Library/Countable.thy	Library/Diagonalize.thy Library/Dlist.thy	\
+  Library/Countable.thy Library/Diagonalize.thy Library/Dlist.thy	\
   Library/Efficient_Nat.thy Library/Enum.thy Library/Eval_Witness.thy	\
   Library/Executable_Set.thy Library/Float.thy				\
   Library/Formal_Power_Series.thy Library/Fraction_Field.thy		\
@@ -417,15 +417,14 @@
   Library/List_Prefix.thy Library/List_lexord.thy Library/Mapping.thy	\
   Library/Monad_Syntax.thy Library/More_List.thy Library/More_Set.thy	\
   Library/Multiset.thy Library/Nat_Bijection.thy			\
-  Library/Nat_Infinity.thy						\
-  Library/Nested_Environment.thy Library/Numeral_Type.thy		\
-  Library/OptionalSugar.thy Library/Order_Relation.thy			\
-  Library/Permutation.thy Library/Permutations.thy			\
-  Library/Poly_Deriv.thy Library/Polynomial.thy				\
-  Library/Predicate_Compile_Quickcheck.thy Library/Preorder.thy		\
-  Library/Product_Vector.thy Library/Product_ord.thy			\
-  Library/Product_plus.thy Library/Quickcheck_Types.thy 		\
-  Library/Quicksort.thy 						\
+  Library/Nat_Infinity.thy Library/Nested_Environment.thy		\
+  Library/Numeral_Type.thy Library/OptionalSugar.thy			\
+  Library/Order_Relation.thy Library/Permutation.thy			\
+  Library/Permutations.thy Library/Poly_Deriv.thy			\
+  Library/Polynomial.thy Library/Predicate_Compile_Quickcheck.thy	\
+  Library/Preorder.thy Library/Product_Vector.thy			\
+  Library/Product_ord.thy Library/Product_plus.thy			\
+  Library/Quickcheck_Types.thy Library/Quicksort.thy			\
   Library/Quotient_List.thy Library/Quotient_Option.thy			\
   Library/Quotient_Product.thy Library/Quotient_Sum.thy			\
   Library/Quotient_Syntax.thy Library/Quotient_Type.thy			\
@@ -440,7 +439,7 @@
   $(SRC)/Tools/adhoc_overloading.ML Library/positivstellensatz.ML	\
   Library/reflection.ML Library/reify_data.ML				\
   Library/document/root.bib Library/document/root.tex
-	@cd Library; $(ISABELLE_TOOL) usedir -b -f HOL_Library_ROOT.ML $(OUT)/HOL HOL-Library
+	@cd Library; $(ISABELLE_TOOL) usedir -b $(OUT)/HOL HOL-Library
 
 
 ## HOL-Hahn_Banach
diff -r deaef70a8c05 -r 1a1973c00531 src/HOL/Library/HOL_Library_ROOT.ML
--- a/src/HOL/Library/HOL_Library_ROOT.ML	Wed Aug 04 10:51:04 2010 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,5 +0,0 @@
-
-(* Classical Higher-order Logic -- batteries included *)
-
-use_thys ["Library", "List_Prefix", "List_lexord", "Sublist_Order",
-  "Code_Char_chr", "Code_Integer", "Efficient_Nat", "Executable_Set", "Code_Prolog"];
diff -r deaef70a8c05 -r 1a1973c00531 src/HOL/Library/ROOT.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Library/ROOT.ML	Wed Aug 04 10:52:29 2010 +0200
@@ -0,0 +1,5 @@
+
+(* Classical Higher-order Logic -- batteries included *)
+
+use_thys ["Library", "List_Prefix", "List_lexord", "Sublist_Order",
+  "Code_Char_chr", "Code_Integer", "Efficient_Nat", "Executable_Set", "Code_Prolog"];
diff -r deaef70a8c05 -r 1a1973c00531 src/HOL/Library/Sum_Of_Squares.thy
--- a/src/HOL/Library/Sum_Of_Squares.thy	Wed Aug 04 10:51:04 2010 +0200
+++ b/src/HOL/Library/Sum_Of_Squares.thy	Wed Aug 04 10:52:29 2010 +0200
@@ -7,9 +7,9 @@
   multiplication and ordering using semidefinite programming *}
 
 theory Sum_Of_Squares
-imports Complex_Main (* "~~/src/HOL/Decision_Procs/Dense_Linear_Order" *)
+imports Complex_Main
 uses
-  "positivstellensatz.ML"  (* duplicate use!? -- cf. Euclidian_Space.thy *)
+  "positivstellensatz.ML"
   "Sum_Of_Squares/sum_of_squares.ML"
   "Sum_Of_Squares/positivstellensatz_tools.ML"
   "Sum_Of_Squares/sos_wrapper.ML"
diff -r deaef70a8c05 -r 1a1973c00531 src/HOL/Multivariate_Analysis/Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Euclidean_Space.thy	Wed Aug 04 10:51:04 2010 +0200
+++ b/src/HOL/Multivariate_Analysis/Euclidean_Space.thy	Wed Aug 04 10:52:29 2010 +0200
@@ -7,9 +7,10 @@
 theory Euclidean_Space
 imports
   Complex_Main "~~/src/HOL/Decision_Procs/Dense_Linear_Order"
-  Infinite_Set
-  Inner_Product L2_Norm Convex
-uses "positivstellensatz.ML" ("normarith.ML")
+  Infinite_Set Inner_Product L2_Norm Convex
+uses
+  "~~/src/HOL/Library/positivstellensatz.ML"  (* FIXME duplicate use!? *)
+  ("normarith.ML")
 begin
 
 lemma cond_application_beta: "(if b then f else g) x = (if b then f x else g x)"
diff -r deaef70a8c05 -r 1a1973c00531 src/HOL/Predicate_Compile_Examples/ROOT.ML
--- a/src/HOL/Predicate_Compile_Examples/ROOT.ML	Wed Aug 04 10:51:04 2010 +0200
+++ b/src/HOL/Predicate_Compile_Examples/ROOT.ML	Wed Aug 04 10:52:29 2010 +0200
@@ -1,2 +1,2 @@
 use_thys ["Predicate_Compile_Examples", "Predicate_Compile_Quickcheck_Examples", "Specialisation_Examples"];
-use_thys ["Code_Prolog_Examples"];
+if getenv "PROLOG_HOME" = "" then () else use_thys ["Code_Prolog_Examples"];
diff -r deaef70a8c05 -r 1a1973c00531 src/HOL/Subst/AList.thy
--- a/src/HOL/Subst/AList.thy	Wed Aug 04 10:51:04 2010 +0200
+++ b/src/HOL/Subst/AList.thy	Wed Aug 04 10:52:29 2010 +0200
@@ -1,28 +1,26 @@
-(*  ID:         $Id$
+(*  Title:      HOL/Subst/AList.thy
     Author:     Martin Coen, Cambridge University Computer Laboratory
     Copyright   1993  University of Cambridge
-
 *)
 
-header{*Association Lists*}
+header {* Association Lists *}
 
 theory AList
 imports Main
 begin
 
-consts alist_rec  :: "[('a*'b)list, 'c, ['a, 'b, ('a*'b)list, 'c]=>'c] => 'c"
-primrec
+primrec alist_rec :: "[('a*'b)list, 'c, ['a, 'b, ('a*'b)list, 'c]=>'c] => 'c"
+where
   "alist_rec [] c d = c"
-  "alist_rec (p # al) c d = d (fst p) (snd p) al (alist_rec al c d)"
+| "alist_rec (p # al) c d = d (fst p) (snd p) al (alist_rec al c d)"
 
-consts assoc      :: "['a,'b,('a*'b) list] => 'b"
-primrec
+primrec assoc :: "['a,'b,('a*'b) list] => 'b"
+where
   "assoc v d [] = d"
-  "assoc v d (p # al) = (if v = fst p then snd p else assoc v d al)"
+| "assoc v d (p # al) = (if v = fst p then snd p else assoc v d al)"
 
 lemma alist_induct:
-    "[| P([]);    
-        !!x y xs. P(xs) ==> P((x,y)#xs) |]  ==> P(l)"
+    "P [] \<Longrightarrow> (!!x y xs. P xs \<Longrightarrow> P ((x,y) # xs)) \<Longrightarrow> P l"
   by (induct l) auto
 
 end
diff -r deaef70a8c05 -r 1a1973c00531 src/HOL/Subst/Subst.thy
--- a/src/HOL/Subst/Subst.thy	Wed Aug 04 10:51:04 2010 +0200
+++ b/src/HOL/Subst/Subst.thy	Wed Aug 04 10:52:29 2010 +0200
@@ -1,34 +1,36 @@
-(*  Title:      Subst/Subst.thy
-    ID:         $Id$
+(*  Title:      HOL/Subst/Subst.thy
     Author:     Martin Coen, Cambridge University Computer Laboratory
     Copyright   1993  University of Cambridge
 *)
 
-header{*Substitutions on uterms*}
+header {* Substitutions on uterms *}
 
 theory Subst
 imports AList UTerm
 begin
 
-consts
+primrec
   subst :: "'a uterm => ('a * 'a uterm) list => 'a uterm"  (infixl "<|" 55)
+where
+  subst_Var: "(Var v <| s) = assoc v (Var v) s"
+| subst_Const: "(Const c <| s) = Const c"
+| subst_Comb: "(Comb M N <| s) = Comb (M <| s) (N <| s)"
+
 notation (xsymbols)
   subst  (infixl "\<lhd>" 55)
-primrec
-  subst_Var:      "(Var v \<lhd> s) = assoc v (Var v) s"
-  subst_Const:  "(Const c \<lhd> s) = Const c"
-  subst_Comb:  "(Comb M N \<lhd> s) = Comb (M \<lhd> s) (N \<lhd> s)"
 
 definition
-  subst_eq :: "[('a*('a uterm)) list,('a*('a uterm)) list] => bool"  (infixr "=$=" 52) where
-  "r =$= s \<longleftrightarrow> (\<forall>t. t \<lhd> r = t \<lhd> s)"
+  subst_eq :: "[('a*('a uterm)) list,('a*('a uterm)) list] => bool"  (infixr "=$=" 52)
+  where "r =$= s \<longleftrightarrow> (\<forall>t. t \<lhd> r = t \<lhd> s)"
+
 notation (xsymbols)
   subst_eq  (infixr "\<doteq>" 52)
 
 definition
-  comp :: "[('a*('a uterm)) list, ('a*('a uterm)) list] => ('a*('a uterm)) list"
-    (infixl "<>" 56) where
-  "al <> bl = alist_rec al bl (%x y xs g. (x,y \<lhd> bl)#g)"
+  comp :: "('a * 'a uterm) list \<Rightarrow> ('a * 'a uterm) list \<Rightarrow> ('a* 'a uterm) list"
+    (infixl "<>" 56)
+  where "al <> bl = alist_rec al bl (%x y xs g. (x,y \<lhd> bl) # g)"
+
 notation (xsymbols)
   comp  (infixl "\<lozenge>" 56)
 
@@ -42,7 +44,7 @@
 
 
 
-subsection{*Basic Laws*}
+subsection {* Basic Laws *}
 
 lemma subst_Nil [simp]: "t \<lhd> [] = t"
   by (induct t) auto
@@ -54,9 +56,8 @@
   apply (case_tac "t = Var v")
    prefer 2
    apply (erule rev_mp)+
-   apply (rule_tac P =
-         "%x. x \<noteq> Var v --> ~(Var v \<prec> x) --> x \<lhd> (v,t\<lhd>s) #s = x\<lhd>s" 
-       in uterm.induct)
+   apply (rule_tac P = "%x. x \<noteq> Var v \<longrightarrow> ~(Var v \<prec> x) \<longrightarrow> x \<lhd> (v,t\<lhd>s) #s = x\<lhd>s" 
+     in uterm.induct)
      apply auto
   done
 
diff -r deaef70a8c05 -r 1a1973c00531 src/HOL/Subst/UTerm.thy
--- a/src/HOL/Subst/UTerm.thy	Wed Aug 04 10:51:04 2010 +0200
+++ b/src/HOL/Subst/UTerm.thy	Wed Aug 04 10:52:29 2010 +0200
@@ -1,52 +1,52 @@
-(*  ID:         $Id$
+(*  Title:      HOL/Subst/UTerm.thy
     Author:     Martin Coen, Cambridge University Computer Laboratory
     Copyright   1993  University of Cambridge
 *)
 
-header{*Simple Term Structure for Unification*}
+header {* Simple Term Structure for Unification *}
 
 theory UTerm
 imports Main
 begin
 
-text{*Binary trees with leaves that are constants or variables.*}
+text {* Binary trees with leaves that are constants or variables. *}
 
 datatype 'a uterm =
     Var 'a
   | Const 'a
   | Comb "'a uterm" "'a uterm"
 
-consts vars_of :: "'a uterm => 'a set"
-primrec
+primrec vars_of :: "'a uterm => 'a set"
+where
   vars_of_Var:   "vars_of (Var v) = {v}"
-  vars_of_Const: "vars_of (Const c) = {}"
-  vars_of_Comb:  "vars_of (Comb M N) = (vars_of(M) Un vars_of(N))"
+| vars_of_Const: "vars_of (Const c) = {}"
+| vars_of_Comb:  "vars_of (Comb M N) = (vars_of(M) Un vars_of(N))"
 
-consts occs :: "'a uterm => 'a uterm => bool"   (infixl "<:" 54) 
+primrec occs :: "'a uterm => 'a uterm => bool"   (infixl "<:" 54) 
+where
+  occs_Var: "u <: (Var v) = False"
+| occs_Const: "u <: (Const c) = False"
+| occs_Comb: "u <: (Comb M N) = (u = M | u = N | u <: M | u <: N)"
+
 notation (xsymbols)
   occs  (infixl "\<prec>" 54)
-primrec
-  occs_Var:   "u \<prec> (Var v) = False"
-  occs_Const: "u \<prec> (Const c) = False"
-  occs_Comb:  "u \<prec> (Comb M N) = (u=M | u=N | u \<prec> M | u \<prec> N)"
 
-consts
-  uterm_size ::  "'a uterm => nat"
-primrec
-  uterm_size_Var:   "uterm_size (Var v) = 0"
-  uterm_size_Const: "uterm_size (Const c) = 0"
-  uterm_size_Comb:  "uterm_size (Comb M N) = Suc(uterm_size M + uterm_size N)"
+primrec uterm_size ::  "'a uterm => nat"
+where
+  uterm_size_Var: "uterm_size (Var v) = 0"
+| uterm_size_Const: "uterm_size (Const c) = 0"
+| uterm_size_Comb: "uterm_size (Comb M N) = Suc(uterm_size M + uterm_size N)"
 
 
-lemma vars_var_iff: "(v \<in> vars_of(Var(w))) = (w=v)"
+lemma vars_var_iff: "(v \<in> vars_of (Var w)) = (w = v)"
   by auto
 
-lemma vars_iff_occseq: "(x \<in> vars_of(t)) = (Var(x) \<prec> t | Var(x) = t)"
+lemma vars_iff_occseq: "(x \<in> vars_of t) = (Var x \<prec> t | Var x = t)"
   by (induct t) auto
 
 
 text{* Not used, but perhaps useful in other proofs *}
-lemma occs_vars_subset: "M\<prec>N \<Longrightarrow> vars_of(M) \<subseteq> vars_of(N)"
+lemma occs_vars_subset: "M \<prec> N \<Longrightarrow> vars_of M \<subseteq> vars_of N"
   by (induct N) auto
 
 
@@ -54,7 +54,7 @@
     "vars_of M Un vars_of N \<subseteq> (vars_of M Un A) Un (vars_of N Un B)"
   by blast
 
-lemma finite_vars_of: "finite(vars_of M)"
+lemma finite_vars_of: "finite (vars_of M)"
   by (induct M) auto
 
 end
diff -r deaef70a8c05 -r 1a1973c00531 src/HOL/Subst/Unifier.thy
--- a/src/HOL/Subst/Unifier.thy	Wed Aug 04 10:51:04 2010 +0200
+++ b/src/HOL/Subst/Unifier.thy	Wed Aug 04 10:52:29 2010 +0200
@@ -1,26 +1,26 @@
-(*  ID:         $Id$
+(*  Title:      HOL/Subst/Unifier.thy
     Author:     Martin Coen, Cambridge University Computer Laboratory
     Copyright   1993  University of Cambridge
 
 *)
 
-header{*Definition of Most General Unifier*}
+header {* Definition of Most General Unifier *}
 
 theory Unifier
 imports Subst
 begin
 
 definition
-  Unifier   :: "[('a * 'a uterm)list, 'a uterm, 'a uterm] => bool" where
-  "Unifier s t u \<longleftrightarrow> t <| s = u <| s"
+  Unifier :: "('a * 'a uterm) list \<Rightarrow> 'a uterm \<Rightarrow> 'a uterm \<Rightarrow> bool"
+  where "Unifier s t u \<longleftrightarrow> t <| s = u <| s"
 
 definition
-  MoreGeneral :: "[('a * 'a uterm)list, ('a * 'a uterm)list] => bool" (infixr ">>" 52) where
-  "r >> s \<longleftrightarrow> (\<exists>q. s =$= r <> q)"
+  MoreGeneral :: "('a * 'a uterm) list \<Rightarrow> ('a * 'a uterm) list \<Rightarrow> bool"  (infixr ">>" 52)
+  where "r >> s \<longleftrightarrow> (\<exists>q. s =$= r <> q)"
 
 definition
-  MGUnifier :: "[('a * 'a uterm)list, 'a uterm, 'a uterm] => bool" where
-  "MGUnifier s t u \<longleftrightarrow> Unifier s t u & (\<forall>r. Unifier r t u --> s >> r)"
+  MGUnifier :: "('a * 'a uterm) list \<Rightarrow> 'a uterm \<Rightarrow> 'a uterm \<Rightarrow> bool"
+  where "MGUnifier s t u \<longleftrightarrow> Unifier s t u & (\<forall>r. Unifier r t u --> s >> r)"
 
 definition
   Idem :: "('a * 'a uterm)list => bool" where
@@ -30,17 +30,17 @@
 lemmas unify_defs = Unifier_def MoreGeneral_def MGUnifier_def
 
 
-subsection{*Unifiers*}
+subsection {* Unifiers *}
 
 lemma Unifier_Comb [iff]: "Unifier s (Comb t u) (Comb v w) = (Unifier s t v & Unifier s u w)"
   by (simp add: Unifier_def)
 
 
-lemma Cons_Unifier: "[| v ~: vars_of t; v ~: vars_of u; Unifier s t u |] ==> Unifier ((v,r)#s) t u"
+lemma Cons_Unifier: "v \<notin> vars_of t \<Longrightarrow> v \<notin> vars_of u \<Longrightarrow> Unifier s t u \<Longrightarrow> Unifier ((v, r) #s) t u"
   by (simp add: Unifier_def repl_invariance)
 
 
-subsection{* Most General Unifiers*}
+subsection {* Most General Unifiers *}
 
 lemma mgu_sym: "MGUnifier s t u = MGUnifier s u t"
   by (simp add: unify_defs eq_commute)
@@ -64,26 +64,26 @@
   done
 
 
-subsection{*Idempotence*}
+subsection {* Idempotence *}
 
-lemma Idem_Nil [iff]: "Idem([])"
+lemma Idem_Nil [iff]: "Idem []"
   by (simp add: Idem_def)
 
-lemma Idem_iff: "Idem(s) = (sdom(s) Int srange(s) = {})"
+lemma Idem_iff: "Idem s = (sdom s Int srange s = {})"
   by (simp add: Idem_def subst_eq_iff invariance dom_range_disjoint)
 
-lemma Var_Idem [intro!]: "~ (Var(v) <: t) ==> Idem([(v,t)])"
+lemma Var_Idem [intro!]: "~ (Var v <: t) ==> Idem [(v,t)]"
   by (simp add: vars_iff_occseq Idem_iff srange_iff empty_iff_all_not)
 
 lemma Unifier_Idem_subst: 
-  "[| Idem(r); Unifier s (t<|r) (u<|r) |]  
-    ==> Unifier (r <> s) (t <| r) (u <| r)"
+  "Idem(r) \<Longrightarrow> Unifier s (t<|r) (u<|r) \<Longrightarrow>
+    Unifier (r <> s) (t <| r) (u <| r)"
   by (simp add: Idem_def Unifier_def comp_subst_subst)
 
 lemma Idem_comp:
-  "[| Idem(r);  Unifier s (t <| r) (u <| r);  
-      !!q. Unifier q (t <| r) (u <| r) ==> s <> q =$= q  
-    |] ==> Idem(r <> s)"
+  "Idem r \<Longrightarrow> Unifier s (t <| r) (u <| r) \<Longrightarrow>
+      (!!q. Unifier q (t <| r) (u <| r) \<Longrightarrow> s <> q =$= q) \<Longrightarrow>
+    Idem (r <> s)"
   apply (frule Unifier_Idem_subst, blast) 
   apply (force simp add: Idem_def subst_eq_iff)
   done
diff -r deaef70a8c05 -r 1a1973c00531 src/HOL/Subst/Unify.thy
--- a/src/HOL/Subst/Unify.thy	Wed Aug 04 10:51:04 2010 +0200
+++ b/src/HOL/Subst/Unify.thy	Wed Aug 04 10:52:29 2010 +0200
@@ -1,10 +1,9 @@
-(*  ID:         $Id$
+(*  Title:      HOL/Subst/Unify.thy
     Author:     Konrad Slind, Cambridge University Computer Laboratory
     Copyright   1997  University of Cambridge
-
 *)
 
-header{*Unification Algorithm*}
+header {* Unification Algorithm *}
 
 theory Unify
 imports Unifier
@@ -27,7 +26,7 @@
 *}
 
 definition
-   unifyRel :: "(('a uterm * 'a uterm) * ('a uterm * 'a uterm)) set" where
+  unifyRel :: "(('a uterm * 'a uterm) * ('a uterm * 'a uterm)) set" where
   "unifyRel = inv_image (finite_psubset <*lex*> measure uterm_size)
       (%(M,N). (vars_of M Un vars_of N, M))"
    --{*Termination relation for the Unify function:
diff -r deaef70a8c05 -r 1a1973c00531 src/HOLCF/IsaMakefile
--- a/src/HOLCF/IsaMakefile	Wed Aug 04 10:51:04 2010 +0200
+++ b/src/HOLCF/IsaMakefile	Wed Aug 04 10:52:29 2010 +0200
@@ -107,8 +107,8 @@
   Library/Strict_Fun.thy \
   Library/Sum_Cpo.thy \
   Library/HOLCF_Library.thy \
-  Library/HOLCF_Library_ROOT.ML
-	@$(ISABELLE_TOOL) usedir -f HOLCF_Library_ROOT.ML $(OUT)/HOLCF Library
+  Library/ROOT.ML
+	@$(ISABELLE_TOOL) usedir $(OUT)/HOLCF Library
 
 
 ## HOLCF-IMP
diff -r deaef70a8c05 -r 1a1973c00531 src/HOLCF/Library/HOLCF_Library_ROOT.ML
--- a/src/HOLCF/Library/HOLCF_Library_ROOT.ML	Wed Aug 04 10:51:04 2010 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,1 +0,0 @@
-use_thys ["HOLCF_Library"];
diff -r deaef70a8c05 -r 1a1973c00531 src/HOLCF/Library/ROOT.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOLCF/Library/ROOT.ML	Wed Aug 04 10:52:29 2010 +0200
@@ -0,0 +1,1 @@
+use_thys ["HOLCF_Library"];
diff -r deaef70a8c05 -r 1a1973c00531 src/Pure/Isar/isar_cmd.ML
--- a/src/Pure/Isar/isar_cmd.ML	Wed Aug 04 10:51:04 2010 +0200
+++ b/src/Pure/Isar/isar_cmd.ML	Wed Aug 04 10:52:29 2010 +0200
@@ -391,7 +391,7 @@
     val thy = Toplevel.theory_of state;
     val thy_session = Present.session_name thy;
 
-    val all_thys = sort Thy_Info.thy_ord (thy :: Theory.ancestors_of thy);
+    val all_thys = rev (thy :: Theory.ancestors_of thy);
     val gr = all_thys |> map (fn node =>
       let
         val name = Context.theory_name node;
diff -r deaef70a8c05 -r 1a1973c00531 src/Pure/ProofGeneral/pgip_isabelle.ML
--- a/src/Pure/ProofGeneral/pgip_isabelle.ML	Wed Aug 04 10:51:04 2010 +0200
+++ b/src/Pure/ProofGeneral/pgip_isabelle.ML	Wed Aug 04 10:52:29 2010 +0200
@@ -80,9 +80,9 @@
                NONE => (NONE, NONE)
              | SOME fname =>
                let val path = Path.explode fname in
-                 case Thy_Load.test_file Path.current path of
-                   SOME _ => (SOME (PgipTypes.pgipurl_of_path path), NONE)
-                 | NONE => (NONE, SOME fname)
+                 if can (Thy_Load.check_file [Path.current]) path
+                 then (SOME (PgipTypes.pgipurl_of_path path), NONE)
+                 else (NONE, SOME fname)
                end);
     in
         { descr=descr, url=url, line=line, column=column, char=NONE, length=NONE }
diff -r deaef70a8c05 -r 1a1973c00531 src/Pure/System/isar.ML
--- a/src/Pure/System/isar.ML	Wed Aug 04 10:51:04 2010 +0200
+++ b/src/Pure/System/isar.ML	Wed Aug 04 10:52:29 2010 +0200
@@ -68,8 +68,7 @@
 
 fun find_and_undo _ [] = error "Undo history exhausted"
   | find_and_undo which ((prev, tr) :: hist) =
-      ((case Toplevel.init_of tr of SOME name => Thy_Info.kill_thy name | NONE => ());
-        if which (Toplevel.name_of tr) then (prev, hist) else find_and_undo which hist);
+      if which (Toplevel.name_of tr) then (prev, hist) else find_and_undo which hist;
 
 in
 
diff -r deaef70a8c05 -r 1a1973c00531 src/Pure/Thy/present.ML
--- a/src/Pure/Thy/present.ML	Wed Aug 04 10:51:04 2010 +0200
+++ b/src/Pure/Thy/present.ML	Wed Aug 04 10:52:29 2010 +0200
@@ -462,7 +462,7 @@
 
     val files_html = files |> map (fn (raw_path, loadit) =>
       let
-        val path = #1 (Thy_Load.check_file dir raw_path);
+        val path = #1 (Thy_Load.check_file [dir] raw_path);
         val base = Path.base path;
         val base_html = html_ext base;
         val _ = add_file (Path.append html_prefix base_html,
diff -r deaef70a8c05 -r 1a1973c00531 src/Pure/Thy/thy_info.ML
--- a/src/Pure/Thy/thy_info.ML	Wed Aug 04 10:51:04 2010 +0200
+++ b/src/Pure/Thy/thy_info.ML	Wed Aug 04 10:52:29 2010 +0200
@@ -15,7 +15,6 @@
   val is_finished: string -> bool
   val master_directory: string -> Path.T
   val loaded_files: string -> Path.T list
-  val thy_ord: theory * theory -> order
   val remove_thy: string -> unit
   val kill_thy: string -> unit
   val use_thys: string list -> unit
@@ -144,8 +143,6 @@
   fun merge _ = empty;
 );
 
-val thy_ord = int_ord o pairself Update_Time.get;
-
 
 (* remove theory *)
 
@@ -238,12 +235,13 @@
 fun required_by _ [] = ""
   | required_by s initiators = s ^ "(required by " ^ show_path (rev initiators) ^ ")";
 
-fun load_thy initiators update_time (deps: deps) text dir name parent_thys =
+fun load_thy initiators update_time (deps: deps) text name parent_thys =
   let
     val _ = kill_thy name;
     val _ = priority ("Loading theory " ^ quote name ^ required_by " " initiators);
 
     val {master = (thy_path, _), ...} = deps;
+    val dir = Path.dir thy_path;
     val pos = Path.position thy_path;
     val uses = map (apfst Path.explode) (#3 (Thy_Header.read pos text));
     fun init () =
@@ -317,7 +315,7 @@
                   let
                     val text = (case opt_text of SOME text => text | NONE => File.read thy_path);
                     val update_time = serial ();
-                  in Task (parent_names, load_thy initiators update_time dep text dir' name) end);
+                  in Task (parent_names, load_thy initiators update_time dep text name) end);
         in (all_current, new_entry name parent_names task tasks') end)
   end;
 
diff -r deaef70a8c05 -r 1a1973c00531 src/Pure/Thy/thy_load.ML
--- a/src/Pure/Thy/thy_load.ML	Wed Aug 04 10:51:04 2010 +0200
+++ b/src/Pure/Thy/thy_load.ML	Wed Aug 04 10:52:29 2010 +0200
@@ -22,8 +22,7 @@
   val master_directory: theory -> Path.T
   val require: Path.T -> theory -> theory
   val provide: Path.T * (Path.T * File.ident) -> theory -> theory
-  val test_file: Path.T -> Path.T -> (Path.T * File.ident) option
-  val check_file: Path.T -> Path.T -> Path.T * File.ident
+  val check_file: Path.T list -> Path.T -> Path.T * File.ident
   val check_thy: Path.T -> string -> Path.T * File.ident
   val deps_thy: Path.T -> string ->
    {master: Path.T * File.ident, text: string, imports: string list, uses: Path.T list}
@@ -110,45 +109,37 @@
 
 (* check files *)
 
-local
-
-exception NOT_FOUND of Path.T list * Path.T;
-
-fun try_file dir src_path =
+fun get_file dirs src_path =
   let
-    val prfxs = search_path dir src_path;
     val path = Path.expand src_path;
     val _ = Path.is_current path andalso error "Bad file specification";
-    val result =
-      prfxs |> get_first (fn prfx =>
-        let val full_path = File.full_path (Path.append prfx path)
-        in Option.map (pair full_path) (File.ident full_path) end);
   in
-    (case result of
-      SOME res => res
-    | NONE => raise NOT_FOUND (prfxs, path))
+    dirs |> get_first (fn dir =>
+      let val full_path = File.full_path (Path.append dir path) in
+        (case File.ident full_path of
+          NONE => NONE
+        | SOME id => SOME (full_path, id))
+      end)
   end;
 
-in
-
-fun test_file dir file =
-  SOME (try_file dir file) handle NOT_FOUND _ => NONE;
+fun check_file dirs file =
+  (case get_file dirs file of
+    SOME path_id => path_id
+  | NONE => error ("Could not find file " ^ quote (Path.implode file) ^
+      "\nin " ^ commas_quote (map Path.implode dirs)));
 
-fun check_file dir file =
-  try_file dir file handle NOT_FOUND (prfxs, path) =>
-    error ("Could not find file " ^ quote (Path.implode path) ^
-      "\nin " ^ commas_quote (map Path.implode prfxs));
-
-fun check_thy dir name = check_file dir (Thy_Header.thy_path name);
-
-end;
+fun check_thy master_dir name =
+  let
+    val thy_file = Thy_Header.thy_path name;
+    val dirs = search_path master_dir thy_file;
+  in check_file dirs thy_file end;
 
 
 (* theory deps *)
 
-fun deps_thy dir name =
+fun deps_thy master_dir name =
   let
-    val master as (thy_path, _) = check_thy dir name;
+    val master as (thy_path, _) = check_thy master_dir name;
     val text = File.read thy_path;
     val (name', imports, uses) = Thy_Header.read (Path.position thy_path) text;
     val _ = Thy_Header.consistent_name name name';
@@ -179,7 +170,7 @@
   let
     val {master_dir, provided, ...} = Files.get thy;
     fun current (src_path, (_, id)) =
-      (case test_file master_dir src_path of
+      (case get_file [master_dir] src_path of
         NONE => false
       | SOME (_, id') => id = id');
   in can check_loaded thy andalso forall current provided end;
@@ -190,15 +181,15 @@
 (* provide files *)
 
 fun provide_file src_path thy =
-  provide (src_path, check_file (master_directory thy) src_path) thy;
+  provide (src_path, check_file [master_directory thy] src_path) thy;
 
 fun use_ml src_path =
   if is_none (Context.thread_data ()) then
-    ML_Context.eval_file (#1 (check_file Path.current src_path))
+    ML_Context.eval_file (#1 (check_file [Path.current] src_path))
   else
     let
       val thy = ML_Context.the_global_context ();
-      val (path, id) = check_file (master_directory thy) src_path;
+      val (path, id) = check_file [master_directory thy] src_path;
 
       val _ = ML_Context.eval_file path;
       val _ = Context.>> Local_Theory.propagate_ml_env;