# HG changeset patch
# User wenzelm
# Date 1343144086 -7200
# Node ID cb03acfae21160af81fbbf39656b7bb8b7bebdfa
# Parent  819f7a5f3e7fab39bd3221ca1c7e2cbd07d93915
modernized imports;

diff -r 819f7a5f3e7f -r cb03acfae211 src/HOL/Decision_Procs/ex/Approximation_Ex.thy
--- 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 {*
diff -r 819f7a5f3e7f -r cb03acfae211 src/HOL/Decision_Procs/ex/Commutative_Ring_Ex.thy
--- 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"
diff -r 819f7a5f3e7f -r cb03acfae211 src/HOL/Decision_Procs/ex/Dense_Linear_Order_Ex.thy
--- 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
diff -r 819f7a5f3e7f -r cb03acfae211 src/HOL/IMP/Abs_Int_Den/Abs_Int_den0_fun.thy
--- 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"
diff -r 819f7a5f3e7f -r cb03acfae211 src/HOL/IMP/Abs_Int_ITP/Abs_Int0_ITP.thy
--- 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"
diff -r 819f7a5f3e7f -r cb03acfae211 src/HOL/IMP/Abs_Int_ITP/Abs_Int1_const_ITP.thy
--- 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"
diff -r 819f7a5f3e7f -r cb03acfae211 src/HOL/IMP/Abs_Int_ITP/Abs_Int2_ITP.thy
--- 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
diff -r 819f7a5f3e7f -r cb03acfae211 src/HOL/IMP/Abs_Int_ITP/Abs_Int2_ivl_ITP.thy
--- 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"