# HG changeset patch
# User wenzelm
# Date 1492783931 -7200
# Node ID 1bf7b5dc34c88342da59dab0033c62a84f83055a
# Parent  b6250ee6ce79912b754da4a61654eaea86054e6d
clarified imports;

diff -r b6250ee6ce79 -r 1bf7b5dc34c8 src/HOL/Proofs/Lambda/WeakNorm.thy
--- a/src/HOL/Proofs/Lambda/WeakNorm.thy	Fri Apr 21 15:26:24 2017 +0200
+++ b/src/HOL/Proofs/Lambda/WeakNorm.thy	Fri Apr 21 16:12:11 2017 +0200
@@ -6,8 +6,7 @@
 section \<open>Weak normalization for simply-typed lambda calculus\<close>
 
 theory WeakNorm
-imports LambdaType NormalForm "~~/src/HOL/Library/Old_Datatype"
-  "~~/src/HOL/Library/Code_Target_Int"
+imports LambdaType NormalForm "HOL-Library.Old_Datatype" "HOL-Library.Code_Target_Int"
 begin
 
 text \<open>
diff -r b6250ee6ce79 -r 1bf7b5dc34c8 src/HOL/ROOT
--- a/src/HOL/ROOT	Fri Apr 21 15:26:24 2017 +0200
+++ b/src/HOL/ROOT	Fri Apr 21 16:12:11 2017 +0200
@@ -449,8 +449,7 @@
   *}
   options [print_mode = "no_brackets",
     parallel_proofs = 0, quick_and_dirty = false]
-  theories [document = false]
-    "~~/src/HOL/Library/Code_Target_Int"
+  sessions "HOL-Library"
   theories
     Eta
     StrongNorm