--- a/src/HOL/Decision_Procs/ex/Approximation_Ex.thy Tue Jul 24 17:33:19 2012 +0200
+++ b/src/HOL/Decision_Procs/ex/Approximation_Ex.thy Tue Jul 24 17:34:46 2012 +0200
@@ -1,7 +1,7 @@
(* Author: Johannes Hoelzl <hoelzl@in.tum.de> 2009 *)
theory Approximation_Ex
-imports Complex_Main "~~/src/HOL/Decision_Procs/Approximation"
+imports Complex_Main "../Approximation"
begin
text {*
--- a/src/HOL/Decision_Procs/ex/Commutative_Ring_Ex.thy Tue Jul 24 17:33:19 2012 +0200
+++ b/src/HOL/Decision_Procs/ex/Commutative_Ring_Ex.thy Tue Jul 24 17:34:46 2012 +0200
@@ -3,7 +3,7 @@
header {* Some examples demonstrating the comm-ring method *}
theory Commutative_Ring_Ex
-imports Commutative_Ring
+imports "../Commutative_Ring"
begin
lemma "4*(x::int)^5*y^3*x^2*3 + x*z + 3^5 = 12*x^7*y^3 + z*x + 243"
--- a/src/HOL/Decision_Procs/ex/Dense_Linear_Order_Ex.thy Tue Jul 24 17:33:19 2012 +0200
+++ b/src/HOL/Decision_Procs/ex/Dense_Linear_Order_Ex.thy Tue Jul 24 17:34:46 2012 +0200
@@ -3,7 +3,7 @@
header {* Examples for Ferrante and Rackoff's quantifier elimination procedure *}
theory Dense_Linear_Order_Ex
-imports "~~/src/HOL/Decision_Procs/Dense_Linear_Order"
+imports "../Dense_Linear_Order"
begin
lemma
--- a/src/HOL/IMP/Abs_Int_Den/Abs_Int_den0_fun.thy Tue Jul 24 17:33:19 2012 +0200
+++ b/src/HOL/IMP/Abs_Int_Den/Abs_Int_den0_fun.thy Tue Jul 24 17:34:46 2012 +0200
@@ -3,7 +3,7 @@
header "Denotational Abstract Interpretation"
theory Abs_Int_den0_fun
-imports "~~/src/HOL/ex/Interpretation_with_Defs" Big_Step
+imports "~~/src/HOL/ex/Interpretation_with_Defs" "../Big_Step"
begin
subsection "Orderings"
--- a/src/HOL/IMP/Abs_Int_ITP/Abs_Int0_ITP.thy Tue Jul 24 17:33:19 2012 +0200
+++ b/src/HOL/IMP/Abs_Int_ITP/Abs_Int0_ITP.thy Tue Jul 24 17:34:46 2012 +0200
@@ -5,7 +5,7 @@
theory Abs_Int0_ITP
imports "~~/src/HOL/ex/Interpretation_with_Defs"
"~~/src/HOL/Library/While_Combinator"
- Collecting
+ "../Collecting"
begin
subsection "Orderings"
--- a/src/HOL/IMP/Abs_Int_ITP/Abs_Int1_const_ITP.thy Tue Jul 24 17:33:19 2012 +0200
+++ b/src/HOL/IMP/Abs_Int_ITP/Abs_Int1_const_ITP.thy Tue Jul 24 17:34:46 2012 +0200
@@ -1,7 +1,7 @@
(* Author: Tobias Nipkow *)
theory Abs_Int1_const_ITP
-imports Abs_Int1_ITP Abs_Int_Tests
+imports Abs_Int1_ITP "../Abs_Int_Tests"
begin
subsection "Constant Propagation"
--- a/src/HOL/IMP/Abs_Int_ITP/Abs_Int2_ITP.thy Tue Jul 24 17:33:19 2012 +0200
+++ b/src/HOL/IMP/Abs_Int_ITP/Abs_Int2_ITP.thy Tue Jul 24 17:34:46 2012 +0200
@@ -1,7 +1,7 @@
(* Author: Tobias Nipkow *)
theory Abs_Int2_ITP
-imports Abs_Int1_ITP Vars
+imports Abs_Int1_ITP "../Vars"
begin
instantiation prod :: (preord,preord) preord
--- a/src/HOL/IMP/Abs_Int_ITP/Abs_Int2_ivl_ITP.thy Tue Jul 24 17:33:19 2012 +0200
+++ b/src/HOL/IMP/Abs_Int_ITP/Abs_Int2_ivl_ITP.thy Tue Jul 24 17:34:46 2012 +0200
@@ -1,7 +1,7 @@
(* Author: Tobias Nipkow *)
theory Abs_Int2_ivl_ITP
-imports Abs_Int2_ITP Abs_Int_Tests
+imports Abs_Int2_ITP "../Abs_Int_Tests"
begin
subsection "Interval Analysis"